Quantifier structure in search based procedures for QBFs

ABSTRACT

The best currently available solvers for Quantified Boolean Formulas (QBFs) process their input in prenex form, i. e., all the quantifiers have to appear in the prefix of the formula separated from the purely propositional part representing the matrix. However, in many QBFs deriving from applications, the propositional part is intertwined with the quantifier structure. To tackle this problem, the standard approach is to first convert them in prenex form, thereby loosing structural information about the prefix.In this paper we show that conversion to prenex form is not necessary, i. e., that it is relatively easy to extend current search based solvers in order to exploit the original quantifier structure, i. e., to handle non prenex QBFs. Further, we show that the conversion can lead to the exploration of search spaces bigger than the space explored by solvers handling non prenex QBFs. To validate our claims, we implemented our ideas in the state-of-the-art search based solver QUBE, and conducted an extensive experimental analysis. The results show that very substantial speedups can be obtained.

REFERENCES

• 1: Abdelwaheb Ayari , David A. Basin, Bounded Model Construction for Monadic Second-Order Logics, Proceedings of the 12th International Conference on Computer Aided Verification, p.99-112, July 15-19, 2000
• 2: M. Benedetti. Quantifier Trees for QBFs. In Proc. SAT'05.
• 3: D. Le Berre, L. Simon, and A. Tacchella. Challenges in the QBF arena: the SAT'03 evaluation of QBF solvers. In Proc. SAT'03.
• 4: A. Biere. Resolve and Expand. In Proc. SAT'04.
• 5: Marco Cadoli , Andrea Giovanardi , Marco Schaerf, An algorithm to evaluate quantified Boolean formulae, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.262-267, July 1998, Madison, Wisconsin, United States
• 6: U. Egly, M. Seidl, H. Tompits, and M. Zolda. Comparing Different Prenexing Strategies for QBFs. In Proc. SAT'03.
• 7: Zhaohui Fu , Yinlei Yu , Sharad Malik, Considering Circuit Observability Don't Cares in CNF Satisfiability, Proceedings of the conference on Design, Automation and Test in Europe, p.1108-1113, March 07-11, 2005 [doi>10.1109/DATE.2005.102]
• 8: Ariel Fuxman , Lin Liu , John Mylopoulos , Marco Pistore , Marco Roveri , Paolo Traverso, Specifying and analyzing early requirements in Tropos, Requirements Engineering, v.9 n.2, p.132-150, May 2004 [doi>10.1007/s00766-004-0191-7]
• 9: 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
• 10: 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]
• 11: E. Giunchiglia, M. Narizzano, and A. Tacchella. QUBE: an Efficient QBF solver. In Proc. FMCAD' 04.
• 12: 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
• 13: M. Mneimneh and K. Sakallah. Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. In Proc. SAT' 03.
• 14: C. H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.
• 15: Christoph Scholl , Bernd Becker, Checking equivalence for partial implementations, Proceedings of the 38th conference on Design automation, p.238-243, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378471]
• 16: D. Sheridan. The optimality of a fast CNF conversion and its use with SAT. In Proc. SAT' 04.
• 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]