march_dl

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

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.

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** ]