The march_dl Sat solver is an upgraded version of the successful march_eq Sat solver, which won two categories in the Sat 2004 competition. For a detailed description of the latter, we refer to [2]. Like march_eq, march_dl integrates equivalence reasoning into a DPLL architecture and uses lookahead heuristics to determine the branch variable in all nodes of the DPLL search-tree. The main improvements in march_dl are:

• additional pre-processing techniques: (1) An iterative full root- lookahead procedure before and after the 3-Sat transformation, and (2) the addition of many ternary constraint resolvents;
• a more dynamic PartialLookahead procedure. Currently, the number of pre-selected variables is based on the number of detected failed literals;
• implementation of a double (second level) lookahead - inspired by Li [1];
• increased readability of the source-code.

The pre-processor of march dl, reduces the formula at hand prior to calling the main solving (DPLL) procedure. Earlier versions already contained unit-clause and binary equivalence propagation, as well as equivalence reasoning, a 3-Sat translator, and finally a full - using all free variables - iterative root-lookahead.
Two new features were added: First, the full iterative root-lookahead is executed twice. (i) Before the 3-Sat transformation to reduce the number of dummy variables (required by the translator), and (ii) afterwards, because lookahead on these dummies could further reduce the size of the formula.
Second, the addition of constraint resolvents appeared fruitful [2]. Therefore, a procedure was implemented in the pre-processor that adds ternary constraint resolvents that could be made by performing a double lookahead on all pairs of literals occurring in ternary clauses.

As a lookahead Sat solver, the branch rule of march_dl is based on a lookahead evaluation function (Diff). The applied Diff measures the reduction of CNF- and equivalence-clauses between two formulas and in a weighted manner. The solver differs from the straight-forward lookahead architecture in two aspects: (1) lookahead is performed on a subset of the free (unfixed) variables, and (2) if a certain lookahead significantly reduces the formula, the DoubleLookahead procedure is called to check whether this lookahead will eventually result in a conflict. Algorithms below show the pseudo-code of this architecture.

The partial behavior of the lookahead procedure is implemented by performing lookahead only on variables in set : At the beginning of each node, this set is filled by pre-selection heuristics based on an approximation function of Diff. In contrast to earlier versions of march, the size of is not fixed to a percentage of the original number of variables. Currently, its size equals a constant times the average number of detected failed literals.
The DoubleLookahead procedure is called when (see algorithm 1). We denote by that many clauses in are reduced clauses of . More specific, clauses in that are satisfied in are not counted. If , then there is a relatively high probability that during DoubleLookahead( ) will contain the empty clause ( ), forcing to be satisfiability equivalent to .
Lookahead on literals that occur sporadically in the formula will rarely result in a conflict. Therefore, it seems reasonable to restrict the number of literals that are evaluated during the DoubleLookahead procedure. This set, denoted by , contains both literals of still unfixed variables in .

• timestamps: A timestamp structure in the lookahead phase enables the construction of a PartialLookahead procedure which does not require 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. All these resolvents 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.

- Chu Min Li. A constrained-based approach to narrow search trees for satisfiability. Information processing letters 71 (1999), 75-80. [ link ]

- Marijn Heule, Joris van Zwieten, Mark Dufour and Hans van Maaren. March_eq: Implementing Additional Reasoning into an Efficient Lookahead Sat Solver. SAT 2004 Springer LNCS 3542 (2005), 345-359. [ .pdf ]