Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts

ABSTRACT

Boolean satisfiability (SAT) solvers are used heavily in hardware and software verification tools for checking satisfiability of Boolean formulas. Most state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjunctive normal form (CNF). We present a new SAT solver that operates on the negation normal form (NNF) of the given Boolean formulas/circuits. The NNF of a formula is usually more succinct than the CNF of the formula in terms of the number of variables. Our algorithm applies the DPLL algorithm to the graph-based representations of NNF formulas. We adapt the idea of the two-watched-literal scheme from CNF SAT solvers in order to efficiently carry out Boolean Constraint Propagation (BCP), a key task in the DPLL algorithm. We evaluate the new solver on a large collection of Boolean circuit benchmarks obtained from formal verification problems. The new solver outperforms the top solvers of the SAT 2007 competition and SAT-Race 2008 in terms of run time on a large majority of the benchmarks.

REFERENCES

• 1: AIGER, http://fmv.jku.at/aiger.
• 2: Hardware model checking competition, http://fmv.jku.at/hwmcc07/.
• 3: Minisat sat solver. http://minisat.se/.
• 4: Picosat sat solver. http://fmv.jku.at/picosat/.
• 5: Rsat sat solver. http://reasoning.cs.ucla.edu/rsat/.
• 6: SAT competition 2007, www.satcompetition.org/2007/.
• 7: P. B. Andrews. An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Kluwer Academic Publishers, second edition, 2002.
• 8: A. Biere. Picosat essentials. Journal on Boolean Satisfiability, Boolean Modeling and Computation (JSAT), 4:75--97, 2008.
• 9: N. Eén and A. Biere. Effective Preprocessing in SAT Through Variable and Clause Elimination. In SAT, pages 61--75, 2005.
• 10: N. Eén, A. Mishchenko, and N. Sörensson. Applying Logic Synthesis for Speeding Up SAT. In SAT, pages 272--286, 2007.
• 11: N. Eén and N. Sörensson. An Extensible SAT-solver. In SAT, pages 502--518, 2003.
• 12: M. K. Ganai, P. Ashar, A. Gupta, L. Zhang, and S. Malik. Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT solver. In DAC, 2002.
• 13: E. Goldberg and Y. Novikov. BerkMin: A Fast and Robust Sat-Solver. In DATE, 2002.
• 14: H. Jain. Verification using satisfiability checking, predicate abstraction, and craig interpolation. Technical Report CMU-CS-08-146, SCS, CMU, 2008.
• 15: H. Jain, C. Bartzis, and E. M. Clarke. Satisfiability checking of non-clausal formulas using general matings. In SAT, pages 75--89, 2006.
• 16: Feng Lu, Li-C. Wang, Kwang-Ting Cheng, and Ric C.-Y. Huang. A Circuit SAT Solver With Signal Correlation Guided Learning. In DATE, 2003.
• 17: J. P. Marques-Silva and K. A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. In ICCAD, pages 220--227, November 1996.
• 18: M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In DAC, pages 530--535, June 2001.
• 19: K. Pipatsrisawat and A. Darwiche. A lightweight component caching scheme for satisfiability solvers. In SAT, pages 294--299, 2007.
• 20: C. Thiffault, F. Bacchus, and T. Walsh. Solving Non-clausal Formulas with DPLL Search. In SAT, 2004.
• 21: G. S. Tseitin. On the complexity of derivation in propositional calculus. In Studies in Constructive Maths and Mathematical Logic, pages 115--125, 1968.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING

General Terms:
Algorithms, Design, Verification

Keywords:
Boolean satisfiability, DPLL, NNF, verification