A SAT-based solver for Q-ALL SAT

ABSTRACT

Although the satisfiability problem (SAT) is NP-complete, state-of-the-art solvers for SAT can solve instances that are considered to be very hard. Emerging applications demand to solve even more complex problems residing at the second or higher levels of the polynomial hierarchy. We identify such a problem, called Q-ALL SAT, that arises in a variety of applications. We have designed a solution algorithm for Q-ALL SAT that employs a SAT solver and thus exploits the recent advances of SAT solvers. In addition, a heuristic is applied to reduce the number of instances that are to be solved by the SAT solver. A learning scheme improves the performance of that heuristic. Test results of a first implementation of the proposed algorithm confirm that this is a very promising approach.

REFERENCES

• 1: Marco Cadoli , Marco Schaerf , Andrea Giovanardi , Massimo Giovanardi, An Algorithm to Evaluate Quantified Boolean Formulae and Its Experimental Evaluation, Journal of Automated Reasoning, v.28 n.2, p.101-142, February 2002 [doi>10.1023/A:1015019416843]
• 2: Thomas Eiter , Georg Gottlob, The complexity of logic-based abduction, Journal of the ACM (JACM), v.42 n.1, p.3-42, Jan. 1995 [doi>10.1145/200836.200838]
• 3: 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
• 4: Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Backjumping for quantified Boolean logic satisfiability, Artificial Intelligence, v.145 n.1-2, p.99-120, April 2003 [doi>10.1016/S0004-3702(02)00373-9]
• 5: M. Mneimneh and K. Sakallah. Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, 2003.
• 6: C. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
• 7: D. Ranjan, D. Tang, and S. Malik. A comparative study of 2qbf algorithms. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), 2004.
• 8: Anja Remshagen , Klaus Truemper, An Effective Algorithm for the Futile Questioning Problem, Journal of Automated Reasoning, v.34 n.1, p.31-47, January 2005 [doi>10.1007/s10817-005-0981-8]
• 9: J. Rintanen. Constructing conditional plans by a theorem prover. Journal of Artificial Intelligence Research, 10:323--352, 1999.
• 10: 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
• 11: SAT 2005. Proceedings of the Eighth International Conference on Theory and Applications of Satisfiability Testing. Fahiem Bacchus and Toby Walsh (Eds.), Springer Verlag, Lecture Notes in Computer Science 3569, 2005.
• 12: SAT Competitions. http://www.satcompetition.org. Daniel Le Berre and Laurent Simon (Organizing committee). 2002--2005.
• 13: Klaus Truemper, Design of Logic-based Intelligent Systems, Wiley-Interscience, 2004
• 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: 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
• 16: 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
• 17: Lintao Zhang , Sharad Malik, Conflict driven learning in a quantified Boolean Satisfiability solver, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.442-449, November 10-14, 2002, San Jose, California [doi>10.1145/774572.774637]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.6 Logic Programming

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computational logic

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.6 Learning

General Terms:
Algorithms

Keywords:
learning, logic programming, quantified Boolean formula