📄 An Extensible SAT-solver

Summary

Modern conflict-driven SAT techniques are well described in the literature, but the low-level details needed to implement them were mostly hidden in large solver codebases. That makes building a new solver, or adapting an existing one to a specific domain such as electronic design automation, slow and error-prone. Eén and Sörensson address this gap by presenting MiniSat, a deliberately minimal yet complete and efficient solver. They distilled it from their earlier solvers Satzoo and Satnik. The paper walks through the code in a style readable by C++ or Java programmers. It covers DPLL-style search, clause learning following GRASP, and watched-literal propagation with dynamic variable ordering following Chaff. Beyond the standard features, MiniSat offers an incremental interface: callers can solve sequences of related problems under temporary unit assumptions. It also provides a lightweight hook for adding arbitrary boolean constraint types. The result is a compact, modifiable reference implementation that lets researchers and practitioners build domain-specific SAT extensions quickly.

Key points

• MiniSat's original C++ source is under 600 lines, excluding comments, and is freely downloadable.
• The API centres on a few calls: newVar(), addClause(), simplifyDB() and solve(assumptions). After a satisfiable run, the model is available in a public vector.
• Solving under unit assumptions is undone after each call. Making the early non-incremental Satzoo comply with this interface required only 5 extra lines of code.
• General constraints plug into all three solver layers: representation, inference (propagation) and search (conflict analysis). Optional undo lists support constraints that must be updated on backtracking.
• An appendix lists Satzoo features omitted from MiniSat. Satzoo won two categories of the SAT 2003 Competition. The omitted features include:
  • an initial burst of random variable orders;
  • a static variable ordering used for at least 5000 conflicts, which the authors consider the most important omission;
  • roughly 1% random branching;
  • equivalent-variable substitution;
  • pseudo-boolean constraints.