×

Solving QBF with counterexample guided refinement. (English) Zbl 1351.68254

Summary: This article puts forward the application of Counterexample Guided Abstraction Refinement (CEGAR) in solving the well-known PSPACE-complete problem of quantified Boolean formulas (QBF). The article studies the application of CEGAR in two scenarios. In the first scenario, CEGAR is used to expand quantifiers of the formula and subsequently a satisfiability (SAT) solver is applied. First it is shown how to do that for two levels of quantification and then it is generalized for arbitrary number of levels by recursion. It is also shown that these ideas can be generalized to non-prenex and non-CNF QBF solvers. In the second scenario, CEGAR is employed as an additional learning technique in an existing DPLL-based QBF solver. Experimental evaluation of the implemented prototypes shows that the CEGAR-driven solver outperforms existing solvers on a number of benchmark families and that the DPLL solver benefits from the additional type of learning.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] H. Kleine Büning, U. Bubeck, Theory of quantified Boolean formulas, in: [71], 2009, pp. 735-760.
[2] Benedetti, M.; Mangassarian, H., QBF-based formal verification: experience and perspectives, J. Satisf. Boolean Model. Comput., 5, 1-4, 133-191, (2008) · Zbl 1172.68538
[3] Rintanen, J., Asymptotically optimal encodings of conformant planning in QBF, (AAAI Conference on Artificial Intelligence, (2007), AAAI Press), 1045-1050
[4] Schaefer, M.; Umans, C., Completeness in the polynomial-time hierarchy: a compendium, SIGACT News, 33, 3, 32-49, (2002)
[5] E. Giunchiglia, P. Marin, M. Narizzano, Reasoning with quantified Boolean formulas, in: [71], 2009, pp. 761-780.
[6] Giunchiglia, E.; Marin, P.; Narizzano, M., Qube 7.0 system description, J. Satisf. Boolean Model. Comput., 7, 83-88, (2010)
[7] Benedetti, M., Evaluating QBFs via symbolic skolemization, (International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR, (2004), Springer), 285-300 · Zbl 1108.68569
[8] Biere, A., Resolve and expand, (International Conference on Theory and Applications of Satisfiability Testing, SAT, (2004)), 238-246
[9] Lonsing, F.; Biere, A., Nenofex: expanding NNF for QBF solving, (International Conference on Theory and Applications of Satisfiability Testing, SAT, (2008), Springer), 196-210 · Zbl 1138.68546
[10] Goultiaeva, A.; Bacchus, F., Exploiting QBF duality on a circuit representation, (AAAI Conference on Artificial Intelligence, (2010), AAAI Press), 71-76
[11] Bubeck, U.; Kleine Büning, H., Bounded universal expansion for preprocessing QBF, (International Conference on Theory and Applications of Satisfiability Testing, SAT, (2007)), 244-257 · Zbl 1214.68331
[12] E. Giunchiglia, P. Marin, M. Narizzano, sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning, in: [69], 2010, pp. 85-98. · Zbl 1306.68157
[13] F. Lonsing, A. Biere, Failed literal detection for QBF, in: [72], 2011, pp. 259-272. · Zbl 1330.68118
[14] Samulowitz, H.; Davies, J.; Bacchus, F., Preprocessing QBF, (International Conference on Principles and Practice of Constraint Programming, CP, (2006), Springer), 514-529
[15] Samulowitz, H.; Bacchus, F., Binary clause reasoning in QBF, (International Conference on Theory and Applications of Satisfiability Testing, SAT, (2006), Springer), 353-367 · Zbl 1187.68265
[16] Biere, A.; Lonsing, F.; Seidl, M., Blocked clause elimination for QBF, (International Conference on Automated Deduction, CADE, (2011)), 101-115 · Zbl 1341.68181
[17] Zhang, L.; Malik, S., Conflict driven learning in a quantified Boolean satisfiability solver, (International Conference on Computer-Aided Design, ICCAD, (2002)), 442-449
[18] Pan, G.; Vardi, M. Y., Symbolic decision procedures for QBF, (International Conference on Principles and Practice of Constraint Programming, CP, (2004), Springer), 453-467 · Zbl 1152.68570
[19] Benedetti, M., Skizzo: a suite to evaluate and certify qbfs, (International Conference on Automated Deduction, CADE, (2005)), 369-376 · Zbl 1135.68550
[20] Clarke, E. M.; Grumberg, O.; Jha, S.; Lu, Y.; Veith, H., Counterexample-guided abstraction refinement for symbolic model checking, J. ACM, 50, 5, 752-794, (2003) · Zbl 1325.68145
[21] Letz, R., Lemma and model caching in decision procedures for quantified Boolean formulas, (Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX, (2002)), 160-175 · Zbl 1015.68173
[22] M. Janota, J. Marques-Silva, Abstraction-based algorithm for 2QBF, in: [72], 2011, pp. 230-244. · Zbl 1330.68115
[23] Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E. M., Solving QBF with counterexample guided refinement, (International Conference on Theory and Applications of Satisfiability Testing, SAT, (2012)), 114-128 · Zbl 1273.68178
[24] Tseitin, G. S., On the complexity of derivation in propositional calculus, Stud. Constr. Math. Math. Log., 2, 115-125, (1970)
[25] Plaisted, D. A.; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304, (1986) · Zbl 0636.68119
[26] Papadimitriou, C. H., Computational complexity, (1994), Addison-Wesley · Zbl 0833.68049
[27] Narodytska, N.; Legg, A.; Bacchus, F.; Ryzhyk, L.; Walker, A., Solving games without controllable predecessor, (Computer Aided Verification, CAV, (2014), Springer), 533-540
[28] Kleine Büning, H.; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf. Comput., 117, 1, 12-18, (1995) · Zbl 0828.68045
[29] C.M. Li, F. Manyà, MaxSAT, hard and soft constraints, in: [71], 2009, pp. 613-631.
[30] Rosa, E. D.; Giunchiglia, E.; Maratea, M., Solving satisfiability problems with preferences, Constraints, 15, 4, 485-515, (2010) · Zbl 1208.68199
[31] N. Eén, N. Sörensson, An extensible SAT-solver, in: [73], 2003, pp. 502-518.
[32] de Moura, L. M.; Rueß, H.; Sorea, M., Lazy theorem proving for bounded model checking over infinite domains, (International Conference on Automated Deduction, CADE, (2002), Springer), 438-455 · Zbl 1072.68602
[33] Barrett, C. W.; Dill, D. L.; Stump, A., Checking satisfiability of first-order formulas by incremental translation to SAT, (Computer Aided Verification, CAV, (2002), Springer-Verlag), 236-249 · Zbl 1010.68531
[34] Cadoli, M.; Giovanardi, A.; Schaerf, M., An algorithm to evaluate quantified Boolean formulae, (National Conference on Artificial Intelligence, (1998), John Wiley & Sons Ltd), 262-267
[35] Klieber, W., Formal verification using quantified Boolean formulas (QBF), (2014), Carnegie Mellon University, Ph.D. thesis
[36] Zhang, L., Solving QBF by combining conjunctive and disjunctive normal forms, (AAAI Conference on Artificial Intelligence, (2006), AAAI Press), 143-150
[37] Lonsing, F.; Biere, A., Depqbf: a dependency-aware QBF solver, J. Satisf. Boolean Model. Comput., 7, 2-3, 71-76, (2010)
[38] QBF-library, the quantified Boolean formulas satisfiability library, (2010)
[39] QBF-evaluation, QBF solver evaluation portal, (2010)
[40] Janota, M.; Botterweck, G.; Grigore, R.; Marques-Silva, J., How to complete an interactive configuration process?, (International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM, (2010), Springer), 528-539
[41] Umans, C., The minimum equivalent DNF problem and shortest implicants, J. Comput. Syst. Sci., 63, 4, 597-611, (2001) · Zbl 1006.68053
[42] W. Klieber, S. Sapra, S. Gao, E.M. Clarke, A non-prenex, non-clausal QBF solver with game-state learning, in: [69], 2010, pp. 128-142. · Zbl 1306.68161
[43] Lonsing, F.; Seidl, M.; Van Gelder, A., The QBF gallery: behind the scenes, CoRR · Zbl 1357.68209
[44] Seidl, M., The qpro input format, (2009), available at
[45] A. Goultiaeva, F. Bacchus, Exploiting circuit representations in QBF solving, in: [69], 2010, pp. 333-339. · Zbl 1306.68158
[46] Wintersteiger, C. M.; Hamadi, Y.; de Moura, L. M., Efficiently solving quantified bit-vector formulas, (Formal Methods in Computer-Aided Design, FMCAD, (2010), IEEE), 239-246
[47] Wintersteiger, C. M.; Hamadi, Y.; de Moura, L. M., Efficiently solving quantified bit-vector formulas, Form. Methods Syst. Des., 42, 1, 3-23, (2013) · Zbl 1284.03212
[48] Monniaux, D., Quantifier elimination by lazy model enumeration, (Computer Aided Verification, CAV, (2010)), 585-599
[49] M.N. Mneimneh, K.A. Sakallah, Computing vertex eccentricity in exponentially large graphs: QBF formulation and solution, in: [73], 2003, pp. 411-425. · Zbl 1204.68206
[50] Browning, B.; Remshagen, A., A SAT-based solver for Q-ALL SAT, (ACM Southeast Regional Conference, (2006), ACM), 30-33
[51] Janota, M.; Grigore, R.; Marques-Silva, J., Counterexample guided abstraction refinement algorithm for propositional circumscription, (European Conference on Logics in Artificial Intelligence, JELIA, (2010)), 195-207 · Zbl 1306.68190
[52] Samulowitz, H.; Bacchus, F., Using SAT in QBF, (International Conference on Principles and Practice of Constraint Programming, CP, (2005), Springer), 578-592 · Zbl 1153.68485
[53] Bubeck, U., Model-based transformations for quantified Boolean formulas, (2010), University of Paderborn, Ph.D. thesis · Zbl 1191.68626
[54] Ayari, A.; Basin, D. A., QUBOS: deciding quantified Boolean logic using propositional satisfiability solvers, (Formal Methods in Computer-Aided Design, FMCAD, (2002), Springer), 187-201 · Zbl 1019.68597
[55] Korovin, K., Instantiation-based automated reasoning: from theory to practice, (International Conference on Automated Deduction, CADE, (2009), Springer), 163-166
[56] Goultiaeva, A.; Seidl, M.; Biere, A., Bridging the gap between dual propagation and CNF-based QBF solving, (Design, Automation & Test in Europe, DATE, (2013), EDA Consortium), 811-814
[57] Dvořák, W.; Järvisalo, M.; Wallner, J. P.; Woltran, S., Complexity-sensitive decision procedures for abstract argumentation, (International Conference on Principles of Knowledge Representation and Reasoning, KR, (2012), AAAI Press), 54-64
[58] Chen, H.; Janota, M.; Marques-Silva, J., QBF-based Boolean function bi-decomposition, (Design, Automation & Test in Europe, DATE, (2012), IEEE), 816-819
[59] Morgenstern, A.; Gesell, M.; Schneider, K., Solving games using incremental induction, (Integrated Formal Methods, IFM, (2013), Springer), 177-191
[60] C. Jordan, Ł. Kaiser, Experiments with reduction finding, in: [70], 2013, pp. 192-207. · Zbl 1390.68349
[61] A. Ignatiev, M. Janota, J. Marques-Silva, Quantified maximum satisfiability: a core-guided approach, in: [70], 2013, pp. 250-266. · Zbl 1390.68598
[62] Jo, S.; Matsumoto, T.; Fujita, M., SAT-based automatic rectification and debugging of combinational circuits with LUT insertions, (Asian Test Symposium, (2012), IEEE Computer Society), 19-24
[63] M. Janota, J. Marques-Silva, On propositional QBF expansions and Q-resolution, in: [70], 2013, pp. 67-82. · Zbl 1390.03017
[64] Beyersdorff, O.; Chew, L.; Janota, M., On unification of QBF resolution-based calculi, (Mathematical Foundations of Computer Science, MFCS, (2014), Springer), 81-93 · Zbl 1426.68283
[65] Van Gelder, A., Contributions to the theory of practical quantified Boolean formula solving, (International Conference on Principles and Practice of Constraint Programming, CP, (2012), Springer), 647-663 · Zbl 1390.68585
[66] Balabanov, V.; Jiang, J.-H. R., Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65, (2012) · Zbl 1284.68516
[67] Janota, M.; Marques-Silva, J., Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42, (2015) · Zbl 1309.68168
[68] Beyersdorff, O.; Chew, L.; Janota, M., Proof complexity of resolution-based QBF calculi, (International Symposium on Theoretical Aspects of Computer Science, STACS, (2015)), 76-89 · Zbl 1355.68105
[69] (SAT10, International Conference on Theory and Applications of Satisfiability Testing, SAT, (2010), Springer)
[70] (SAT13, International Conference on Theory and Applications of Satisfiability Testing, SAT, (2013), Springer)
[71] (Handbook of Satisfiability, vol. 185, (2009), IOS Press) · Zbl 1183.68568
[72] (SAT11, International Conference on Theory and Applications of Satisfiability Testing, SAT, (2011), Springer)
[73] (SAT03, International Conference on Theory and Applications of Satisfiability Testing, SAT, (2003), Springer)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.