×

Expansion-based QBF solving versus Q-resolution. (English) Zbl 1309.68168

Summary: This article introduces and studies a proof system \(\forall\)Exp+Res that enables us to refute quantified Boolean formulas (QBFs). The system \(\forall\)Exp+Res operates in two stages: it expands all universal variables through conjunctions and refutes the result by propositional resolution. This approach contrasts with the Q-resolution calculus, which enables refuting QBFs by rules similar to propositional resolution. In practice, Q-resolution enables producing proofs from conflict-driven DPLL-based QBF solvers. The system \(\forall\)Exp+Res can on the other hand certify certain expansion-based solvers. So a natural question is to ask which of the systems, Q-resolution and \(\forall\)Exp+Res, is more powerful? The article gives several partial responses to this question. On the positive side, we show that \(\forall\)Exp+Res can p-simulate tree Q-resolution. On the negative side, we show that \(\forall\)Exp+Res does not p-simulate unrestricted Q-resolution. In the favor of \(\forall\)Exp+Res we show that \(\forall\)Exp+Res is more powerful than a certain fragment of Q-resolution, which is important for DPLL-based QBF solving.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B35 Mechanization of proofs and logical operations
03F20 Complexity of proofs
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Oliva, S., On the complexity of resolution-based proof systems, (March 2013), Departament de Llenguatges i Sistemes Informàtics Universitat Politècnica de Catalunya, Ph.D. thesis
[2] Alekhnovich, M.; Razborov, A. A., Satisfiability, branch-width and tseitin tautologies, Comput. Complexity, 20, 4, 649-678, (2011) · Zbl 1243.68182
[3] Cook, S. A.; Reckhow, R. A., The relative efficiency of propositional proof systems, J. Symbolic Logic, 44, 1, 36-50, (1979) · Zbl 0408.03044
[4] Krajíček, J.; Pudlák, P., Quantified propositional calculi and fragments of bounded arithmetic, MLQ Math. Log. Q., 36, 1, 29-46, (1990) · Zbl 0696.03031
[5] Büning, H. K.; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inform. and Comput., 117, 1, 12-18, (1995) · Zbl 0828.68045
[6] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Clause/term resolution and learning in the evaluation of quantified Boolean formulas, J. Artificial Intelligence Res., 26, 1, 371-416, (2006) · Zbl 1183.68475
[7] U. Egly, On sequent systems and resolution for QBFs, in: Cimatti and Sebastiani [35], pp. 100-113. · Zbl 1273.03161
[8] Van Gelder, A., Contributions to the theory of practical quantified Boolean formula solving, (Milano, M., CP, vol. 7514, (2012), Springer), 647-663 · Zbl 1390.68585
[9] Rintanen, J., Improvements to the evaluation of quantified Boolean formulae, (Dean, T., IJCAI, (1999), Morgan Kaufmann), 1192-1197
[10] Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M., An algorithm to evaluate quantified Boolean formulae and its experimental evaluation, J. Automat. Reason., 28, 2, 101-142, (2002) · Zbl 1002.68165
[11] Zhang, L.; Malik, S., Conflict driven learning in a quantified Boolean satisfiability solver, (ICCAD, (2002)), 442-449
[12] Lonsing, F.; Biere, A., Depqbf: a dependency-aware QBF solver, J. Satisf. Boolean Model. Comput., 7, 2-3, 71-76, (2010)
[13] Giunchiglia, E.; Marin, P.; Narizzano, M., Qube 7.0 system description, J. Satisf. Boolean Model. Comput., 7, 83-88, (2010)
[14] Ayari, A.; Basin, D. A., QUBOS: deciding quantified Boolean logic using propositional satisfiability solvers, (Aagaard, M.; O’Leary, J. W., FMCAD, vol. 2517, (2002), Springer), 187-201 · Zbl 1019.68597
[15] Biere, A., Resolve and expand, (SAT, (2004)), 238-246
[16] Lonsing, F.; Biere, A., Nenofex: expanding NNF for QBF solving, (Büning, H. K.; Zhao, X., SAT, vol. 4996, (2008), Springer), 196-210 · Zbl 1138.68546
[17] M. Janota, W. Klieber, J. Marques-Silva, E.M. Clarke, Solving QBF with counterexample guided refinement, in: Cimatti and Sebastiani [35], pp. 114-128. · Zbl 1273.68178
[18] Bubeck, U.; Büning, H. K., Bounded universal expansion for preprocessing QBF, (Marques-Silva, J.; Sakallah, K. A., SAT, vol. 4501, (2007), Springer), 244-257 · Zbl 1214.68331
[19] Bubeck, U., Model-based transformations for quantified Boolean formulas, (2010), University of Paderborn, Ph.D. thesis · Zbl 1191.68626
[20] Janota, M.; Marques-Silva, J., On propositional QBF expansions and Q-resolution, (Järvisalo, M.; Van Gelder, A., SAT, vol. 7962, (2013), Springer), 67-82 · Zbl 1390.03017
[21] Janota, M.; Marques-Silva, J., ∀exp+res does not p-simulate Q-resolution, (International Workshop on Quantified Boolean Formulas, (2013))
[22] Büning, H. K.; Bubeck, U., Theory of quantified Boolean formulas, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, (2009), IOS Press), 735-760
[23] Bonet, M. L.; Esteban, J. L.; Galesi, N.; Johannsen, J., Exponential separations between restricted resolution and cutting planes proof systems, (39th Annual Symposium on Foundations of Computer Science, FOCS, (1998), IEEE Computer Society), 638-647
[24] Tseitin, G. S., On the complexity of derivations in the propositional calculus, (Slisenko, A. O., Studies in Constructive Mathematics and Mathematical Logic Part II, (1983)) · Zbl 0197.00102
[25] Urquhart, A., The complexity of propositional proofs, Bull. Eur. Assoc. Theor. Comput. Sci., 64, (1998) · Zbl 0912.03026
[26] Beyersdorff, O., Disjoint NP-pairs and propositional proof systems, (2006), Humboldt University Berlin, Ph.D. thesis · Zbl 1119.03059
[27] Cadoli, M.; Schaerf, M.; Giovanardi, A.; Giovanardi, M., An algorithm to evaluate quantified Boolean formulae and its experimental evaluation, J. Automat. Reason., 28, 2, (2002) · Zbl 1002.68165
[28] Janota, M.; Marques-Silva, J., Abstraction-based algorithm for 2QBF, (Sakallah, K. A.; Simon, L., SAT, (2011), Springer), 230-244 · Zbl 1330.68115
[29] Balabanov, V.; Jiang, J.-H. R., Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65, (2012) · Zbl 1284.68516
[30] Craig, W., Linear reasoning. A new form of the Herbrand-Gentzen theorem, J. Symbolic Logic, 22, 3, 250-268, (1957) · Zbl 0081.24402
[31] QBF gallery, http://www.kr.tuwien.ac.at/events/qbfgallery2013/, 2013.
[32] Goerdt, A., Davis-Putnam resolution versus unrestricted resolution, Ann. Math. Artif. Intell., 6, 1-3, 169-184, (1992) · Zbl 0865.03010
[33] Benedetti, M., Evaluating QBFs via symbolic skolemization, (Baader, F.; Voronkov, A., LPAR, vol. 3452, (2004), Springer), 285-300 · Zbl 1108.68569
[34] Alekhnovich, M.; Johannsen, J.; Pitassi, T.; Urquhart, A., An exponential separation between regular and general resolution, Theory Comput., 3, 1, 81-102, (2007) · Zbl 1213.68303
[35] (Cimatti, A.; Sebastiani, R., Proceedings of 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, Trento, Italy, June 17-20, 2012, vol. 7317, (2012), Springer) · Zbl 1268.68009
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.