|
| developers |
 |
|
|
|
|
Marijn Heule
Hans van Maaren
|
|
|
| introduction |
|
|
|
|
|
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.
|
|
|
| pre-processing |
|
|
|
|
|
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.
|
|
|
| architecture |
|
|
|
|
|
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 .
|
|
|
| features |
|
|
|
|
|
- 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.
|
|
|
| references |
|
|
|
|
|
[1] Chu Min Li. A constrained-based approach to narrow search trees for satisfiability.
Information processing letters 71 (1999), 75-80.
[ 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), 345-359.
[ .pdf ]
|
|
|
|
|
March
