Elamur Research⌕
☰
home / papers / 2001 / Chaff: Engineering an Efficient SAT Solver

Chaff: Engineering an Efficient SAT Solver

Paper · 2001 · Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao et al.

Summary

Chaff tackles a central challenge in Electronic Design Automation (EDA) and AI: making complete Boolean Satisfiability (SAT) solving fast on hard, real-world instances. Like most complete solvers, it builds on Davis-Putnam (DP) backtracking search over CNF formulas. Rather than adding sophisticated new pruning or learning techniques, the authors carefully engineered the steps where solvers spend most of their time.

Boolean constraint propagation (BCP) usually accounts for over 90% of runtime, so they redesigned it around a "two watched literals" scheme. A clause is examined only when one of its two watched literals becomes false, and backtracking leaves the watches untouched. They also introduced VSIDS, a cheap decision heuristic that favors literals appearing in recently added clauses.

On DIMACS benchmarks and Velev's microprocessor-verification suites, Chaff ran one to two orders of magnitude faster than GRASP and SATO. It also solved many instances those solvers abandoned. The work shows that low-level engineering, such as reducing memory accesses and cache misses, can matter as much as algorithmic novelty.

Key points

  • BCP takes more than 90% of runtime in most SAT solvers. Chaff's two-watched-literal scheme makes unassigning a variable a constant-time operation. Unlike SATO's head/tail approach, the watches can move in any direction.
  • VSIDS (Variable State Independent Decaying Sum) is a low-overhead branching heuristic biased toward recently added clauses. It is compared against alternatives such as RAND, DLIS, MOMs and BOHM.
  • On VLIW-SAT.1.0, GRASP and SATO each aborted 19 of the first 20 instances, while Chaff solved all 100 in under 10,000 seconds total.
  • On FVP-UNSAT.1.0, GRASP and SATO completed only one easy instance, whereas Chaff finished all 4.
  • The authors report Chaff as roughly 100× faster on hard unsatisfiable instances and at least 10× faster on satisfiable ones. Timeouts were 100 s per instance for DIMACS sets and up to 1000 s for the Velev suites.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of California, BerkeleyBerkeley · United States243 works · 251,774 citations🎓Massachusetts Institute of TechnologyCambridge · United States274 works · 82,013 citations🎓Princeton UniversityPrinceton · United States137 works · 53,849 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksComputational Theory and Mathematics · 496 worksComputer Networks and Communications · 115 works

Cite

Cite as Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik. 2001. Chaff: Engineering an Efficient SAT Solver. DAC 2001, 530–535.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/378239.379017

@inproceedings{moskewicz2001chaff,
  title = {{Chaff: Engineering an Efficient SAT Solver}},
  author = {Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik},
  booktitle = {DAC 2001, 530–535},
  year = {2001},
  doi = {10.1145/378239.379017},
  url = {https://doi.org/10.1145/378239.379017}
}

References

12 references, 0 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Baptista, L., and Marques-Silva, J.P., “Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability,” Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP), September 2000. find
  2. Bayardo, R. and Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances, in Proc. of the 14th Nat. (US) Conf. on Artificial Intelligence (AAAI-97), AAAI Press/The MIT Press, 1997, pp. 203–208. find
  3. Biere, A., Cimatti, A., Clarke, E.M., and Zhu, Y., “Symbolic Model Checking without BDDs,” Tools and Algorithms for the Analysis and Construction of Systems (TACAS'99), number 1579 in LNCS. Springer-Verlag, 1999. (http://www.cs.cmu.edu/~modelcheck/bmc/bmc-benchmarks.html) find
  4. Freeman, J.W., “Improvements to Propositional Satisfiability Search Algorithms,” Ph.D. Dissertation, Department of V 1 =1 -V 1 V 4 -V 7 V 11 V 12 V 15 Implication: V 12 =1 V 4 =0 -V 1 V 4 -V 7 V 11 V 12 V 15 Conflict, Backtrack. V 15 =X V 11 =X V 7 =X V 4 =X V 7 = 0 V 12 =1 -V 1 V 4 -V 7 V 11 V 12 V… find
  5. Kunz, W, and Sotoffel, D., Reasoning in Boolean Networks, Kluwer Academic Publishers, 1997. find
  6. Marques-Silva, J.P., “The Impact of Branching Heuristics in Propositional Satisfiability Algorithms,” Proceedings of the 9th Portuguese Conference on Artificial Intelligence (EPIA), September 1999. find
  7. Marques-Silva, J. P., and Sakallah, K. A., “GRASP: A Search Algorithm for Propositional Satisfiability,” IEEE Transactions on Computers, vol. 48, 506-521, 1999. find
  8. McAllester, D., Selman, B. and Kautz, H.: Evidence for invariants in local search, in Proceedings of AAAI’97, MIT Press, 1997, pp. 321–326. find
  9. Stephan, P., Brayton, R., and Sangiovanni-Vencentelli, A., “Combinational Test Generation Using Satisfiability,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, 1167-1176, 1996. find
  10. Velev, M., FVP-UNSAT.1.0, FVP-UNSAT.2.0, VLIW-SAT.1.0, SSS-SAT.1.0, Superscalar Suite 1.0, Superscalar Suite 1.0a, Available from: http://www.ece.cmu.edu/~mvelev ↗
  11. Velev, M. and Bryant, R., “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,” In Proceedings of the Design Automation Conference, 2001. find
  12. Zhang, H., “SATO: An efficient propositional prover,” Proceedings of the International Conference on Automated Deduction, pages 272-275, July 1997. -V 1 V 4 -V 7 V 11 V 12 V 15 V 15 =0 V 7 =1 V 11 =0 -V 1 V 4 -V 7 V 11 V 12 V 15 -V 1 V 4 -V 7 V 11 V 12 V 15 V 4 =0 -V 1 V 4 -V 7 V 11 V 12 V 15 Figure… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/moskewicz-2001-chaff-engineering-efficient-sat-solver/