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.
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.
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.