This page is kept for reference only. Consider visiting the MiniSat page instead.
Satzoo is a Chaff-like SAT-solver based on watched literals [MZ01] and clause recording [MS99].
It was developed mainly to be able to experiment with new model checking techniques
which requires a tighter integration with the SAT-solver. As such, Satzoo takes a more general
view on what a "SAT" problem could be, and supports solving a number of related SAT-problems by
an incremental SAT interface [WKS01]. Satzoo is also meant to encompass more types of constraints than
just clauses. To prototype this, linear constraints over boolean variables [Bar95] were added to
the solver. The front end thus supports a subset of the CPLEX lp-format along with DIMACS cnf-format.
For lp-files optimization is performed towards the goal function rather than just finding a satisfying assignment.
In the SAT 2003 Competition, Satzoo won the two ``Handmade'' categories, as well as solving both
the most number of series and the most number of instances of all solvers in the first round. Click here for details. NEW -- in the 2004
competition, it defended one of its titles: the satisfiable handmade category.
The techniques used in Satzoo are described in the paper An Extensible SAT-solver,
co-authored by Niklas Sörensson. A shorter version of this paper will appear in the SAT'03 proceedings.
The paper contains a minimal SAT-solver MiniSat, as well as an appendix explaining the difference between this solver
and Satzoo. The source code for MiniSat (available below) should provide a good start for anyone interesting in
extending a modern SAT-solver.
Clause database simplification
- Burst of random variable orders. Before anything else, Satzoo runs several passes of about
10-100 conflicts each with the variable order initiated to random. For satisfiable problems, Satzoo
can sometimes stumble upon the solution by this strategy. For hard (typically unsatisfiable) problems,
important clauses can be learnt in this phase that is outside the "local optimum" that the activity driven
variable heuristic will later get stuck in.
- Static variable ordering based on the structure of the clause database. The second phase of Satzoo
is to compute a static variable ordering taking into account how the variables of different clauses relates
to each other. Variables often occuring together in clauses will be put close in the variable order. Satzoo
uses this static ordering for at least 5000 conflicts and doesn't stop until progress is halted severely.
The static ordering often counters the effect of "shuffling" the problem (changing the order of clauses).
Multiple decision heuristics
- Fixed literal removal. Literals that gets fixed (implied under no assumption)
to false will periodically be removed from the clause database. Likewise for clauses
containing literals that gets fixed to true.
- Equivalent variable substitution. The binary clauses are checked for cyclic
implications. If a cycle is found, a representative is selected and all other variables in
the cycle is replaced by this representative in the clause database. This yields a smaller
database and fewer variables. The simplification is done periodically, but is most important
in the initial phase (some problems can be very redundant).
- Variable activity. This is the standard Chaff activity heuristic. Variables participating
in learnt clauses have their "activity" increased. All activities decay over time. When picking
an unassigned variable for branching, the most active variable is chosen. This heuristic is
employed most of the time.
- Variable of recent importance. Inspired by Berkmin [GY02], occasionally variables from recent
(unsatisfied) recorded clauses are picked.
- Random. About 1% of the time, a random variable is selected for branching. This cracked
many problems during my testing.
- Clauses can be added incrementally. The API of Satzoo allows "solve" to be
run any number of times. Between each solve, clauses can be added.
- Solve method accepts hypothesis. The main "solve"-method of the API accepts a
number of unit clauses that will be treated as assumptions. The assumptions will be temporary
asserted during solving the SAT problem. Afterwards these assumptions are reverted.
In practice, this interface allows for the removal of any set of clauses [ES03].
- Linear constraints can be added. This is a major extension of SAT. Linear programming problems
over boolean variables can be solved. The extension also facilitates for instance MAXSAT and MAXONE.
- Optimization. Satzoo supports optimization towards a specified linear goal function.
- Conversion to clauses. Linear constraints can be converted into clauses. For certain problem this
is faster than using native constraints. The converted problem can also be exported to be used with
another, better (?) solver.
Statically linked binaries for Linux, Solaris, and Windows (through
Cygwin) are available, as well as library and header files for the
``A Davis-Putnam Based Enumeration Algorithm for Linear pseudo-Boolean Optimization''
in Resarch Report, Max-Planck-Institut für Informatik, MPI-I-95-2-003, 1995.
N. Eén, N. Sörensson
``Temporal Induction by Incremental SAT Solving''
First International Workshop on Bounded Model Checking, ENTCS issue 4 volume 89.
E. Goldberg, Y. Novikov
``BerkMin: A Fast and Robust SAT Solver''
in Design Automation and Test in Europe, pages 142--149, 2002.
J.P. Marques-Silva, K.A. Sakallah
``GRASP: A Search Algorithm for Propositional Satisfiability''
in IEEE Transactions on Computers, vol 48, pages 506--521, 1999.
M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, S. Malik
``Chaff: Engineering an Efficient SAT Solver''
in Proc. of the Design Automation Conference, pages 530-535, 2001.
J. Whittemore, J. Kim, K. Sakallah
``SATIRE: a new incremental satisfiability engine''
in Proc. of the 38th conference on Design automation, pages 542--545, 2001.
© Copyright Niklas Eén, 2003