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