




developers 





Marijn Heule
Hans van Maaren
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 searchtree. The main improvements in march_dl are:
 additional preprocessing techniques: (1) An iterative full rootlookahead procedure
before and after the 3SAT transformation, and (2) the addition of many ternary constraint resolvents;
 a more dynamic PartialLookahead procedure. Currently, the number of preselected 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 sourcecode.
The preprocessor of march dl, reduces the formula at hand prior to calling the main solving
(DPLL) procedure. Earlier versions already contained unitclause and binary equivalence
propagation, as well as equivalence reasoning, a 3Sat translator, and finally a full  using all
free variables  iterative rootlookahead.
Two new features were added: First, the full iterative rootlookahead is executed twice.
(i) Before the 3Sat 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 preprocessor 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 equivalenceclauses
between two formulas and in a weighted manner. The solver differs from
the straightforward 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 pseudocode 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 preselection
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 datastructures are used for storing
the binary and ternary clauses. Both are designed to decrease the number of
cache misses in the PartialLookahead procedure.
 treebased 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
datastructure to speedup the lookahead.
[1] Chu Min Li. A constrainedbased approach to narrow search trees for satisfiability.
Information processing letters 71 (1999), 7580.
[ link ].
[2] 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), 345359.
[ .pdf ]
  