• extensive reasoning within the pre-processor: This results in a fast detection of a conflict on several benchmark families and in an increased propagation of unary clauses and binary equivalences while pre-processing the formula.
• 3-Sat translator: Due to its use, many optimisations of the data-structures towards the elementary 3-Sat format become possible.
• partial lookahead: Selection of a small constant number of variables for the lookahead procedure. This requires a clear discrimination between the variables, which is realised by our pre-selection heuristics.
• optimised lookahead: Using special data-structures to reduce the number of cache misses, implication trees to reduce the number of unit propagations and a time-stamp structure to prevent backtracking costs, the lookahead phase is even fast on formulas with many clauses.
• enhanced reasoning in the lookahead phase: Detection of necessary assignments and autarkies, and the addition of binary resolvents, makes it possible to solve much more benchmarks compared to ``pure'' lookahead

1. simplifying: Iterative propagation of all unary clauses and binary equivalences.
2. equivalence reasoning: First all so called equivalence clauses l1 l2 ... ln (where the li are literals, or their negations) are extracted from the CNF and placed in a separate data-structure called Conjunction of Equivalences (CoE). Second, the found CoE is solved using a polynomial algorithm. Unary clauses or binary equivalences found in the solution are iteratively propagated. If no conflict has occurred, the original clause form is used for the not satisfied equivalences. The remaining CoE part is neglected during solving (in contrast to march_eq).
3. two phase 3-Sat translator: In the first phase every pair of literals that occurs multiple times in clauses, is replaced by a single dummy variable and three clauses are added for each pair to make the dummy logically equivalent to the disjunction of the two literals involved. The second phase consists of a straight forward 3-Sat translation.
4. addition of resolvents: Several resolvents of length two and three are added during this stage.
5. full root lookahead: Although partial lookahead appears useful in the lower nodes of the DPLL search tree, performing a full lookahead in the root node practically always results in a speed-up.

The lookahead evaluation function (Diff in short) used in march sums up - in a weighted fashion - the newly created binary clauses in the resulted formula after lookahead on a variable. A new binary clauses x v y is weighted according to equation (1). In this equation occn( l ) refers to the occurrences of literal l in clauses of length n. The final branch decision is based on function H, which is calculated as in line 12 of Algorithm 1. In a node, variable x with the highest H( x ) is selected as branch variable for its two child nodes.

(1)

The partial behaviour of the lookahead is realised by only performing lookahead on variables in set : At the beginning of each node, this set is filled by pre-selection heuristics that are based on a Diff approximation function (Daf). The ranking of variable x is calculated by multiplying Daf(x) and Daf(x). The higher the ranking, the ``better'' the variable. Set contains always a constant number of variables. This constant number depends on the original number of variables.

(2)

Two variants of march have been submitted to the Sat 2004 competition. The first, march_001 performs only lookahead on the "best" 1% of the variables, while the second, march_007 performs only lookahead on the "best" 7%.

• Prohibit equivalent variables from both occurring in : Equivalent variables will have the same Diff, so only one of them is required in .
• Autarky detection: When after a lookahead on x, the resulted formula is an autarky with respect to the formula before the lookahead, x is assigned to true. This generally results in a speed-up while solving satisfiable instances.
• Timestamps: A timestamp structure in the lookahead phase makes it possible to perform PartialLookahead without backtracking.
• Cache optimisations: Two alternative data-structures are used for storing the binary and ternary clauses. Both are designed to decrease the number of cache misses in the PartialLookahead procedure.
• Tree-based lookahead: Before the actual lookahead operations are performed, various implication trees are built of the binary clauses of which both literals occur in . These implications trees are used to decrease the number of unit propagations.
• Necessary assignments: If both x y and x y are detected during the lookahead on x and x , y is assigned to true because it is a necessary assignment.
• Resolvents: Several binary resolvents are added during the solving phase. Those resolvents that are added have the property that they are easily detected during the lookahead phase and that they could increase the number of detected failed literals.
• Restructuring: Before calling procedure PartialLookahead, all satisfied ternary clauses of the prior node are removed from the active data-structure to speed-up the lookahead.