Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver

ABSTRACT

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

REFERENCES

• 1: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 2: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 3: João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999 [doi>10.1109/12.769433]
• 4: M. Schulz, E. Trischler, and T. Sarfert, "SOCRATES: A highly efficient ATPG System," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 7, pp. 126--137, 1988.
• 5: Andreas Kuehlmann , Malay K. Ganai , Viresh Paruthi, Circuit-based Boolean Reasoning, Proceedings of the 38th conference on Design automation, p.232-237, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378470]
• 6: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 7: H. Fujiwara and T. Shimono, "On the Acceleration of Test Generation Algorithms," IEEE Transactions on Computers, vol. C-32, pp. 265--272, 1983.
• 8: P. Goel, "An implicit enumeration algorithm to generate tests for Combinational circuits," IEEE Transactions on Computers, vol. C-30, pp. 215--222, 1981.
• 9: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 10: M. N. Velev, "Benchmark Suites. http://www.ece.cmu.edu/~mvelev," October 2000.

INDEX TERMS

Primary Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Algorithms, Experimentation, Performance, Verification

Keywords:
boolean constraint propagation (BCP), boolean satisfiability (SAT), bounded model checking (BMC), conjunctive normal form (CNF)