Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice

ABSTRACT

Despite the increasing use of QBF solvers, current QBF solvers do not provide for any mechanism to verify their results. This paper demonstrates a methodology for independently validating the results of a DLL based QBF solver using the traces generated during the solving process. It also presents a mechanism to extract small unsatisfiable subformulas, called cores, from unsatisfiable QBF instances.

REFERENCES

• 1: QBF evaluation 2004 benchmarks, available from http://www.mrg.dist.unige.it/qbflib/benchmarks/04secondtestset.tar, 2004.
• 2: R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Convergence testing in term-level bounded model checking. In Proc. CHARME'03, vol. 2860 of LNCS, pp. 348--362, 2003.
• 3: 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]
• 4: M. Cadoli and M. Schaerf. An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. In Highlights of Satisfiability Research in 2000, 2000.
• 5: 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]
• 6: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 7: Uwe Egly , Thomas Eiter , Hans Tompits , Stefan Woltran, Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas, Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on Innovative Applications of Artificial Intelligence, p.417-422, July 30-August 03, 2000
• 8: 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
• 9: G. Gopalakrishnan, Y. Yang, and H. Sivaraj. QB or not QB: An efficient execution verification tool for memory orderings. In Proc. CAV'04, 2004.
• 10: 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
• 11: M. Mneimneh and K. A. Sakallah. Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution. In Proc. SAT'03, vol. 2919 of LNCS, pp. 411--425, 2003.
• 12: 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]
• 13: J. Rintanen. Constructing conditional plans by a theorem-prover. J. of Artificial Intelligence Research, 10:322--352, 1999.
• 14: L. J. Stockmeyer , A. R. Meyer, Word problems requiring exponential time(Preliminary Report), Proceedings of the fifth annual ACM symposium on Theory of computing, p.1-9, April 30-May 02, 1973, Austin, Texas, United States [doi>10.1145/800125.804029]
• 15: Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Analyzing the Intel Itanium memory ordering rules using logic programming and SAT. In Proc. CHARME'03, vol. 2860 of LNCS, pp. 81--95, 2003.
• 16: Y. Yu and S. Malik. yQuaffle QBF solver. available from http://www.princeton.edu/chaff/quaffle.html
• 17: L. Zhang and S. Malik. Conflict driven learning in a quantified Boolean satisfiability solver.
• 18: L. Zhang and S. Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications.
• 19: 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