Chaff: engineering an efficient SAT solver

ABSTRACT

Boolean Satisfiability is probably the most studied of combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO.

References

1. 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.]]
2. 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.]]
3. 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)]]
4. 4.DIMACS benchmarks available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks]]
5. 5.Freeman, J.W., "Improvements to Propositional Satisfiability Search Algorithms," Ph.D. Dissertation, Department of Computer and Information Science, University of Pennsylvania, May 1995.]]
6. 6.Kunz, W, and Sotoffel, D., Reasoning in Boolean Networks, Kluwer Academic Publishers, 1997.]]
7. 7.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.]]
8. 8.Marques-Silva, J. P., and Sakallah, K. A., "GRASP: A Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers, vol. 48, 506-521, 1999.]]
9. 9.McAllester, D., Selman, B. and Kautz, H.: Evidence for invariants in local search, in Proceedings of AAAI'97, MIT Press, 1997, pp. 321-326.]]
10. 10.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.]]
11. 11.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]]
12. 12.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.]]
13. 13.Zhang, H., "SATO: An efficient propositional prover, Proceedings of the International Conference on Automated Deduction, pages 272-275, July 1997.]]

Index Terms

• Applied computing

  • Physical sciences and engineering

    • Engineering

• Computer systems organization

  • Dependable and fault-tolerant systems and networks

• General and reference

  • Cross-computing tools and techniques

    • Performance

• Hardware

  • Robustness

• Networks

  • Network performance evaluation

• Theory of computation

  • Computational complexity and cryptography

    • Interactive proof systems

    • Proof complexity

  • Logic

    • Proof theory