• extensive equivalence reasoning within the pre-processor: Equivalence clauses are extracted and a minimum solution for this equivalence part of the formula is computed.
• 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, makes the lookahead phase is even ``fast'' on formulas with many clauses.
• combined lookahead evaluation: The heuristics in marcheq to evaluate the lookahead are fully optimised towards effectively solving benchmarks containing a considerable number of equivalence clauses.

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, a procedure is called to compute a solution of the CoE which total length of non-tautological equivalence clauses is minimal. Notice that at this point, march_eq takes another strategy than march.
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 combined lookahead evaluation function (Diff in short) used in march_eq combines the evaluation of the reduction of CNF-clauses and the evaluation of the reduction of equivalence clauses. The reduction of the CNF-clauses is measured by counting the newly created binary clauses in the resulted formula after lookahead on a variable. The reduction of the CoE is measured by summing up - in a weighted fashion - all reduced equivalence clauses. A reduced equivalence clause of new length n is weighted using eqn (equation (1)). The Diff is obtained by adding both evaluations. The final branch decision is based on equation 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 an approximation function of the combined evaluation of the lookahead (Ace). The ranking of variable x is calculated by multiplying Ace(x) and Ace(x). The higher the ranking, the "better" the variable. (x), used to obtain Ace(x), refers to the set of all equivalence clauses (denoted as ) in which x occurs, and occ3( x ) refers to the number of occurrences of literal x in ternary clauses.

(2)

Because the computational costs of calculating the above pre-selection heuristics are relatively high, two variants of march_eq are submitted to the Sat 2004 competition: The first, march_eq_010 performs only lookahead on the "best" 10% of the variables, while the second, march_eq_100 performs a full lookahead which is expensive, but at least makes it possible to eliminate the pre-selection heuristics.

• Prohibit equivalent variables from both occurring in : Equivalent variables will have the same Diff, so only one of them is required in .
• 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.
• Binary equivalences: If both x y and x y are detected during the lookahead on x and x, binary equivalence x y is propagated in the CoE data-structure to reduce the length of some equivalence clauses.
• 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.