DEPRICATED! 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.
Features
Initial strategies- 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).
Clause database simplification- 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).
Multiple decision heuristics- 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.
Incremental SAT- 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].
0-1-programming- 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.
Downloads
Statically linked binaries for Linux, Solaris, and Windows (through Cygwin) are available, as well as library and header files for the incremental interface:
References
[Bar95] P. Barth ``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.
[ES03] N. Eén, N. Sörensson ``Temporal Induction by Incremental SAT Solving'' First International Workshop on Bounded Model Checking, ENTCS issue 4 volume 89.
[GY02] E. Goldberg, Y. Novikov ``BerkMin: A Fast and Robust SAT Solver'' in Design Automation and Test in Europe, pages 142--149, 2002.
[MS99] 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.
[MZ01] 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.
[WKS01] 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