×

Building strategies into QBF proofs. (English) Zbl 07356969

Summary: Strategy extraction is of great importance for quantified Boolean formulas (QBF), both in solving and proof complexity. So far in the QBF literature, strategy extraction has been algorithmically performed from proofs. Here we devise the first QBF system where (partial) strategies are built into the proof and are piecewise constructed by simple operations along with the derivation. This has several advantages: (1) lines of our calculus have a clear semantic meaning as they are accompanied by semantic objects; (2) partial strategies are represented succinctly (in contrast to some previous approaches); (3) our calculus has strategy extraction by design; and (4) the partial strategies allow new sound inference steps which are disallowed in previous central QBF calculi such as Q-Resolution and long-distance Q-Resolution. The last item (4) allows us to show an exponential separation between our new system and the previously studied reductionless long-distance resolution calculus. Our approach also naturally lifts to dependency QBFs (DQBF), where it yields the first sound and complete CDCL-style calculus for DQBF, thus opening future avenues into CDCL-based DQBF solving.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Azhar, S.; Peterson, G.; Reif, J., Lower bounds for multiplayer non-cooperative games of incomplete information, J. Comput. Math. Appl., 41, 957-992 (2001) · Zbl 0991.91007 · doi:10.1016/S0898-1221(00)00333-3
[2] Balabanov, V.; Chiang, H-JK; Jiang, J-HR, Henkin quantifiers and Boolean formulae: a certification perspective of DQBF, Theoret. Comput. Sci., 523, 86-100 (2014) · Zbl 1283.03032 · doi:10.1016/j.tcs.2013.12.020
[3] Balabanov, V.; Jiang, J-HR, Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65 (2012) · Zbl 1284.68516 · doi:10.1007/s10703-012-0152-6
[4] Balabanov, V., Jiang, J.-H.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter)models from long-distance resolution proofs. In: Bonet, B., Koenig, S. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 3694-3701. AAAI Press (2015)
[5] Benedetti, M.: sKizzo: a suite to evaluate and certify QBFs. In: Nieuwenhuis, R. (ed.) International Conference on Automated Deduction (CADE), Volume 3632 of Lecture Notes in Computer Science, pp. 369-376. Springer (2005) · Zbl 1135.68550
[6] 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
[7] Beyersdorff, O., Blinkhorn, J. (2016) Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) International Conference on Principles and Practice of Constraint Programming (CP), Volume 9892 of Lecture Notes in Computer Science, pp. 96-112. Springer
[8] Beyersdorff, O.; Blinkhorn, J.; Chew, L.; Schmidt, RA; Suda, M., Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, J. Autom. Reason., 63, 3, 597-623 (2019) · Zbl 1468.03008 · doi:10.1007/s10817-018-9482-4
[9] Beyersdorff, O., Blinkhorn, J., Hinde, L.: Size, cost, and capacity: a semantic technique for hard random QBFs. Log. Methods Comput. Sci. 15(1), 13:1-13:39 (2019) · Zbl 1515.03213
[10] Beyersdorff, O., Blinkhorn, J., Mahajan, M.: Building strategies into QBF proofs. In: Niedermeier, R., Paul, C. (ed.) International Symposium on Theoretical Aspects of Computer Science (STACS), Volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 14:1-14:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019) · Zbl 07559123
[11] Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Sudan, M. (ed.) ACM Conference on Innovations in Theoretical Computer Science (ITCS), pp. 249-260. ACM (2016) · Zbl 1334.68084
[12] Beyersdorff, O.; Chew, L.; Janota, M., New resolution-based QBF calculi and their proof complexity, ACM Trans. Comput. Theory, 11, 4, 26:1-26:42 (2019) · Zbl 1496.68362 · doi:10.1145/3352155
[13] Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: Creignou and Berre [21], pp. 490-499 · Zbl 1475.68431
[14] Beyersdorff, O.; Wintersteiger, CM, International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 10929 of Lecture Notes in Computer Science (2018), Berlin: Springer, Berlin
[15] Bjørner, N., Janota, M., Klieber, W.: On conflicts and strategies in QBF. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) International Conference on Logic for Programming, Artificial Intelligence and Reasoning—Short Presentations (LPAR), Volume 35 of EPiC Series in Computing, pp. 28-41. EasyChair (2015)
[16] Bubeck, U., Büning, H.K.: Dependency quantified Horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 4121 of Lecture Notes in Computer Science, pp. 198-211. Springer (2006) · Zbl 1187.68256
[17] Buss, SR, Towards NP-P via proof complexity and search, Ann. Pure Appl. Log., 163, 7, 906-917 (2012) · Zbl 1257.03086 · doi:10.1016/j.apal.2011.09.009
[18] Cashmore, M., Fox, M., Giunchiglia, E.: Partially grounded planning as quantified Boolean formula. In: Borrajo, D., Kambhampati, S., Oddi, A., Fratini, S. (eds.) International Conference on Automated Planning and Scheduling (ICAPS). AAAI (2013) · Zbl 1327.68211
[19] Cook, SA; Nguyen, P., Logical Foundations of Proof Complexity (2010), Cambridge: Cambridge University Press, Cambridge · Zbl 1206.03051 · doi:10.1017/CBO9780511676277
[20] Cook, SA; Reckhow, RA, The relative efficiency of propositional proof systems, J. Symb. Log., 44, 1, 36-50 (1979) · Zbl 0408.03044 · doi:10.2307/2273702
[21] Creignou, N.; Le Berre, D., International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science (2016), Berlin: Springer, Berlin
[22] Egly, U.; Kronegger, M.; Lonsing, F.; Pfandler, A., Conformant planning as a case study of incremental QBF solving, Ann. Math. Artif. Intell., 80, 1, 21-45 (2017) · Zbl 1409.68253 · doi:10.1007/s10472-016-9501-2
[23] Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K.L., Middeldorp, K.L., Voronkov, A. (eds.) International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Volume 8312 of Lecture Notes in Computer Science, pp. 291-308. Springer (2013) · Zbl 1406.68106
[24] Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay and Margaria [39], pp. 354-370 · Zbl 1452.68118
[25] Finkbeiner, B., Tentrup, L.: Fast DQBF refutation. In: Sinz, C., Egly, U. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 8561 of Lecture Notes in Computer Science, pp. 243-251. Springer (2014) · Zbl 1423.68447
[26] Fröhlich, A., Kovásznai, G., Biere, A.: A DPLL algorithm for solving DQBF. https://arise.or.at/pubpdf/Algorithm_for_Solving__DQBF_.pdf, presented at Workshop on Pragmatics of SAT (POS) (2012)
[27] Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Le Berre, D. (ed.) Workshop on Pragmatics of SAT (POS), Volume 27 of EPiC Series in Computing, pp. 103-116. EasyChair (2014)
[28] Gaspers, S.; Walsh, T., International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science (2017), Berlin: Springer, Berlin
[29] Gitina, K., Wimmer, R., Reimer, S., Sauer, M., Scholl, C., Becker, B.: Solving DQBF through quantifier elimination. In: Nebel, W., Atienza, D. (eds.) Design, Automation & Test in Europe Conference (DATE), pp. 1617-1622. ACM (2015)
[30] Giunchiglia, E.; Narizzano, M.; Tacchella, A., Clause/term resolution and learning in the evaluation of quantified Boolean formulas, J. Artif. Intell. Res., 26, 371-416 (2006) · Zbl 1183.68475 · doi:10.1613/jair.1959
[31] Heule, M., Seidl, M., Biere, A.: Efficient extraction of Skolem functions from QRAT proofs. In: Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 107-114. IEEE (2014)
[32] Heule, MJH; Kullmann, O., The science of brute force, Commun. ACM, 60, 8, 70-79 (2017) · doi:10.1145/3107239
[33] Janota, M.; Lynce, I., International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science (2019), Berlin: Springer, Berlin
[34] Janota, M.; Marques-Silva, J., Expansion-based QBF solving versus Q-resolution, Theor. Comput. Sci., 577, 25-42 (2015) · Zbl 1309.68168 · doi:10.1016/j.tcs.2015.01.048
[35] Büning, HK; Karpinski, M.; Flögel, A., Resolution for quantified Boolean formulas, Inf. Comput., 117, 1, 12-18 (1995) · Zbl 0828.68045 · doi:10.1006/inco.1995.1025
[36] Klieber, W., Sapra, S., Gao, S., Clarke, E.M.: A non-prenex, non-clausal QBF solver with game-state learning. In: Strichman, O., Szeider, S. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 6175 of Lecture Notes in Computer Science, pp. 128-142. Springer (2010) · Zbl 1306.68161
[37] Kontchakov, R., Pulina, L., Sattler, U., Schneider, T., Selmer, P., Wolter, F., Zakharyaschev, M.: Minimal module extraction from DL-lite ontologies using QBF solvers. In: Boutilier, C. (ed.) International Joint Conference on Artificial Intelligence (IJCAI), pp. 836-841. AAAI Press (2009)
[38] Krajíček, J., Bounded Arithmetic, Propositional Logic, and Complexity Theory. Encyclopedia of Mathematics and Its Applications (1995), Cambridge: Cambridge University Press, Cambridge · Zbl 0835.03025
[39] Legay, Axel, Margaria, Tiziana (eds.): International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 10205. Springer, (2017)
[40] Ling, A.C., Singh, D.P., Brown, S.D.: FPGA logic synthesis using quantified Boolean satisfiability. In: Bacchus, F., Walsh, T. (eds.), International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 3569 of Lecture Notes in Computer Science, pp. 444-450. Springer (2005) · Zbl 1128.94308
[41] Mangassarian, H.; Veneris, AG; Benedetti, M., Robust QBF encodings for sequential circuits with applications to verification, debug, and test, IEEE Trans. Comput., 59, 7, 981-994 (2010) · Zbl 1366.94786 · doi:10.1109/TC.2010.74
[42] Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 247-275. Springer (2018) · Zbl 1390.68001
[43] Nordström, J., On the interplay between proof complexity and SAT solving, SIGLOG News, 2, 3, 19-44 (2015) · doi:10.1145/2815493.2815497
[44] Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou and Berre [21], pp. 500-518 · Zbl 1475.68446
[45] Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers and Walsh [28], pp. 298-313 · Zbl 1478.68330
[46] Peitl, T., Slivovsky, F., Szeider, S.: Polynomial-time validation of QCDCL certificates. In: Beyersdorff and Wintersteiger [14], pp. 253-269 · Zbl 1511.68127
[47] Peitl, T., Slivovsky, F., Szeider, S.: Proof complexity of fragments of long-distance Q-resolution. In: Janota and Lynce [33], pp. 319-335 · Zbl 1441.03044
[48] QBFEVAL homepage: http://www.qbflib.org/index_eval.php. Accessed 26 Oct 2018
[49] Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: Kaivola, R., Wahl, T. (eds.) Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 136-143. IEEE (2015)
[50] Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers and Walsh [28], pp. 314-325 · Zbl 1496.03050
[51] Samulowitz, H., Davies, J., Bacchus, F.: Preprocessing QBF. In: Benhamou, F. (ed.) International Conference on Principles and Practice of Constraint Programming (CP), Volume 4204 of Lecture Notes in Computer Science, pp. 514-529. Springer (2006)
[52] Scholl, C., Wimmer, R.: Dependency quantified Boolean formulas: an overview of solution methods and applications—extended abstract. In: Beyersdorff and Wintersteiger [14], pp. 3-16
[53] Silva, J.P.M., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Volume 185 of Frontiers in Artificial Intelligence and Applications, pp. 131-153. IOS Press (2009) · Zbl 1183.68568
[54] Suda, M., Gleiss, B.: Local soundness for QBF calculi. In: Beyersdorff and Wintersteiger [14], pp. 217-234 · Zbl 1508.03045
[55] Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: Janota and Lynce [33], pp. 388-405 · Zbl 1441.68241
[56] Vardi, MY, Boolean satisfiability: theory and engineering, Commun. ACM, 57, 3, 5 (2014) · doi:10.1145/2578043
[57] Wimmer, R., Gitina, K., Nist, J., Scholl, C., Becker, B.: Preprocessing for DQBF. In: Heule, M., Weaver, S. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT), Volume 9340 of Lecture Notes in Computer Science, pp. 173-190. Springer (2015) · Zbl 1471.68264
[58] Wimmer, R., Reimer, S., Marin, P., Becker, B.: HQSpre—an effective preprocessor for QBF and DQBF. In: Legay and Margaria [39], pp. 373-390
[59] Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD), pp. 442-449 (2002)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.