Conflict driven learning in a quantified Boolean Satisfiability solver

ABSTRACT

Within the verification community, there has been a recent increase in interest in Quantified Boolean Formula evaluation (QBF) as many interesting sequential circuit verification problems can be formulated as QBF instances. A closely related research area to QBF is Boolean Satisfiability (SAT). Recent advances in SAT research have resulted in some very efficient SAT solvers. One of the critical techniques employed in these solvers is Conflict Driven Learning. In this paper, we adapt conflict driven learning for application in a QBF setting. We show that conflict driven learning can be regarded as a resolution process on the clauses. We prove that under certain conditions, tautology clauses obtained from resolution in QBF also obey the rules for implication and conflicts of regular (non-tautology) clauses; and therefore they can be treated as regular clauses and used in future search. We have implemented this idea in a new QBF solver called Quaffle and our initial experiments show that conflict driven learning can greatly speed up the solution process for most of the benchmarks we tested.

REFERENCES

• 1: J. Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323--352, 1999
• 2: Mary Sheeran , Satnam Singh , Gunnar Stålmarck, Checking Safety Properties Using Induction and a SAT-Solver, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design, p.108-125, November 01-03, 2000
• 3: 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
• 4: Hans Kleine Büning , Marek Karpinski , Andreas Flögel, Resolution for quantified Boolean formulas, Information and Computation, v.117 n.1, p.12-18, Feb. 15, 1995 [doi>10.1006/inco.1995.1025]
• 5: David A. Plaisted , Armin Biere , Yunshan Zhu, A satisfiability procedure for quantified boolean formulae, Discrete Applied Mathematics, v.130 n.2, p.291-328, 15 August 2003 [doi>10.1016/S0166-218X(02)00409-2]
• 6: 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]
• 7: M. Cadoli, M. Schaerf, A. Giovanardi and M. Giovanardi. An algorithm to evaluate quantified Boolean formulae and its experimental evaluation, in Highlights of Satisfiability Research in the Year 2000, IOS Press, 2000
• 8: Jussi Rintanen, Improvements to the Evaluation of Quantified Boolean Formulae, Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, p.1192-1197, July 31-August 06, 1999
• 9: Jussi Rintanen, Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae, Proceedings of the Artificial Intelligence on Logic for Programming, p.362-376, December 03-07, 2001
• 10: Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability, Proceedings of the First International Joint Conference on Automated Reasoning, p.364-369, June 18-23, 2001
• 11: E. Giunchiglia, M. Narizzano and A. Tacchella. Backjumping for Quangified Boolean Logic Satisfiability. In Proceedings of International Joint Conf. on Artificial Intelligence (IJCAI), 2001
• 12: 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]
• 13: R. Bayard and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances, in Proc. of the 14th Nat. (US) Conf. on Artificial Intelligence (AAAI), 1997
• 14: Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997
• 15: 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]
• 16: Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
• 17: David A. Plaisted , Steven Greenbaum, A structure-preserving clause form translation, Journal of Symbolic Computation, v.2 n.3, p.293-304, Sept. 1986 [doi>10.1016/S0747-7171(86)80028-1]
• 18: E. Giunchiglia, M. Narizzano and A. Tacchella, On the effectiveness of backjumping and trivial truth in quantified boolean formulas satisfiability, in IJCAR workshop on Theory and Application of Quantified Boolean Formulas, 2001
• 19: Gary D. Hachtel , Fabio Somenzi, Logic Synthesis and Verification Algorithms, Kluwer Academic Publishers, Norwell, MA, 2000
• 20: J. Rintanen's benchmark suites are available at <u>http://www.informatik.uni-freiburg.de/~rintanen/qbf.html</u>
• 21: More detailed and expanded experimental results are available at <u>http://ee.princeton.edu/~chaff/Quaffle.php</u>
• 22: Reinhold Letz, Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas, Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, p.160-175, July 30-August 01, 2002
• 23: Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Learning for quantified boolean logic satisfiability, Eighteenth national conference on Artificial intelligence, p.649-654, July 28-August 01, 2002, Edmonton, Alberta, Canada
• 24: Lintao Zhang , Sharad Malik, Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation, Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, p.200-215, September 09-13, 2002

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.1 Design Styles
          Subjects: Sequential circuits

Additional Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Verification

  I. Computing Methodologies
  I.1 SYMBOLIC AND ALGEBRAIC MANIPULATION
      I.1.0 General
      I.1.2 Algorithms
          Subjects: Analysis of algorithms

General Terms:
Algorithms, Design, Experimentation