﻿
 doi:

DOI: 10.3724/SP.J.1001.2011.03859

Journal of Software (软件学报) 2011/22:7 PP.1538-1550

## Heuristic Survey Propagation Algorithm for Solving QBF Problem

• YIN Ming-Hao 1,2   ZHOU Jun-Ping 1,3   SUN Ji-Gui 2,3   GU Wen-Xiang 1
• 1.College of Computer Science, Northeast Normal University,Changchun,130117,China
• 2.Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education,Changchun,130012,China
• 3.College of Computer Science and Technology, Jilin University,Changchun,130012,China

Abstract：
This paper presents a heuristic survey propagation algorithm for solving Quantified Boolean Formulae (QBF) problem. A QBF solver based on the algorithm is designed, namely HSPQBF (heuristic survey propagation algorithm for solving QBF). This solver is a QBF reasoning engine that incorporates Survey Propagation method for problem solving. Using the information obtained from the survey propagation procedure, HSPQBF can select a branch accurately. Furthermore, when handling the branches, HSPQBF uses efficient technology to solve QBF problems, such as unit propagation, conflict driven learning, and satisfiability directed at implication and learning. The experimental results also show that HSPQBF can solve both random and QBF benchmark problems efficiently, which validates the effect of using survey propagation in a QBF solving process.

Key words：artificial intelligence,quantified Boolean formulae problem,QBF(quantified Boolean formulae) solver,factor graph,survey propagation,conflict driven learning,satisfiability directed implication and learning

ReleaseDate：2014-07-21 15:50:31

[1] Garey MR, Johnson DS. Computers and Intractability, A Guide to the Theory of NP-Completeness. San Francisco: W. H. Freeman, 1979.

[2] Pan GQ, Vardi MY. Optimizing a BDD-based modal solver. In: Baader F, ed. Proc. of the 19th Int’l Conf. on Automated Deduction. Berlin, Heidelberg: Springer-Verlag, 2003. 75-89. [doi: 10.1007/978-3-540-45085-6_7]

[3] Rintanen J. Asymptotically optimal encodings of conformant planning in QBF. In: Collins J, Faratin P, Parsons S, eds. Proc. of the 22nd AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 2007. 1045-1050.

[4] Egly U, Eiter T, Tompits H, Woltran S. Solving advanced reasoning tasks using quantified Boolean formulas. In: Collins J, Faratin P, Parsons S, eds. Proc. of the 12th AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 2000. 417-422.

[5] Gent IP, Hoos HH, Rowley AGD, Smyth K. Using stochastic local search to solve quantified Boolean formulae. In: Rossi F, ed. Proc. of the Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer-Verlag, 2003. 348-362.

[6] Gent I, Giunchiglia E, Narizzano M, Rowley A, Tachella A. Watched data structures for QBF solvers. In: Giunchiglia E, Tacchella A, eds. Proc. of the 6th Int’l Conf. on Theory and Applications of Satisfiability Testing. LNCS 2919, Berlin, Heidelberg: Springer-Verlag, 2003. 348-355. [doi: 10.1007/978-3-540-24605-3_3]

[7] Giunchiglia E, Narizzano4 M, Tacchella A. QuBE: A system for deciding quantified Boolean formulas satisfiability. In: Nebel B, ed. Proc. of the 17th Int’l Joint Conf. on Artificial Intelligence. LNCS 2083, Morgan Kaufmann Publishers, 2001. 18-23. [doi: 10.1007/3-540-45744-5_27]

[8] Rintanen J. Partial implicit unfolding in the Davis Putnam procedure for quantified Boolean formulae. In: Nieuwenhuis R, Voronkov A, eds. Proc. of the 8th Int’l Conf. on Logic for Programming, Artificial Intelligence and Reasoning. LNCS 2250, Berlin, Heidelberg: Springer-Verlag, 2001. 362-376. [doi: 10.1007/3-540-45653-8_25]

[9] Zhang LT, Malik S. Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Rossi F, ed. Proc. of the Principles and Practice of Constraint Programming. Berlin, Heidelberg: Springer-Verlag, 2002. 200-215. [doi: 10.1007/3-540-46135-3_14]

[10] Cadoli M, Giovanardi A, Schaerf M. An algorithm to evaluate quantified Boolean formulae. In: Collins J, Faratin P, Parsons S, eds. Proc. of the AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 1998. 262-267.

[11] Monasson R, Zecchina R, Kirkpatrick S, Selman B, Troyansky L. Determining computational complexity from characteristic ‘phase transitions’. Nature, 1999,400(6740):133-137. [doi: 10.1038/22055]

[12] Mézard M, Parisi G, Zecchina R. Analytic and algorithmic solution of random satisfiability problems. Science, 2002, 297(5582):812-815. [doi: 10.1126/science.1073287]

[13] Gent I, Walsh T. Beyond NP: The QSAT phase transition. In: Collins J, Faratin P, Parsons S, eds. Proc. of the AAAI Conf. on Artificial Intelligence. Menlo Park: AAAI Press, 1999. 648-653.

[14] Giunchiglia E, Narizzano M, Tacchella A. Quantified Boolean formulas satisfiability library (QBFLIB). 2001. http://www.qbflib. org/