Soundness of \(\mathcal{Q}\)-resolution with dependency schemes. (English) Zbl 1332.68204
Summary: \(\mathcal{Q}\)-resolution and \(\mathcal{Q}\)-term resolution are proof systems for quantified Boolean formulas (QBFs). We introduce generalizations of these proof systems named \(\mathcal{Q}(D)\)-resolution and \(\mathcal{Q}(D)\)-term resolution. \(\mathcal{Q}(D)\)-resolution and \(\mathcal{Q}(D)\)-term resolution are parameterized by a dependency scheme \(D\) and use more powerful \(\forall\)-reduction and \(\exists\)-reduction rules, respectively. We show soundness of these systems for particular dependency schemes: we prove (1) soundness of \(\mathcal{Q}(D)\)-resolution parameterized by the reflexive resolution-path dependency scheme, and (2) soundness of \(\mathcal{Q}(D)\)-term resolution parameterized by the resolution-path dependency scheme. These results entail soundness of the proof systems used for certificate generation in the state-of-the-art solver DepQBF.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
References:
| [1] | Balabanov, V.; Chiang, H.-J. K.; Jiang, J.-H. R., Henkin quantifiers and Boolean formulae: a certification perspective of DQBF, Theoret. Comput. Sci., 523, 86-100 (2014) · Zbl 1283.03032 |
| [2] | Balabanov, V.; Jiang, J.-H. R., Unified QBF certification and its applications, Form. Methods Syst. Des., 41, 1, 45-65 (2012) · Zbl 1284.68516 |
| [3] | Biere, A.; Cimatti, A.; Clarke, E. M.; Zhu, Y., Symbolic model checking without BDDs, (Cleaveland, R., Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 5th International Conference, TACAS ’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 5th International Conference, TACAS ’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99, Amsterdam, The Netherlands, March 22-28, 1999. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 5th International Conference, TACAS ’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99. Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 5th International Conference, TACAS ’99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’99, Amsterdam, The Netherlands, March 22-28, 1999, Lecture Notes in Computer Science, vol. 1579 (1999), Springer Verlag), 193-207 |
| [4] | Biere, A.; Lonsing, F., Integrating dependency schemes in search-based QBF solvers, (Strichman, O.; Szeider, S., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2010. Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2010, Lecture Notes in Computer Science, vol. 6175 (2010), Springer Verlag), 158-171 · Zbl 1306.68165 |
| [5] | Bjesse, P.; Leonard, T.; Mokkedem, A., Finding bugs in an alpha microprocessor using satisfiability solvers, (Berry, G.; Comon, H.; Finkel, A., Computer Aided Verification, Proceedings of the 13th International Conference. Computer Aided Verification, Proceedings of the 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001 (2001)), 454-464 · Zbl 0996.68578 |
| [6] | Bubeck, U., Model-Based Transformations for Quantified Boolean Formulas, Dissertations in Artificial Intelligence, vol. 329 (2010), IOS Press/Akademische Verlagsgesellschaft AKA · Zbl 1191.68626 |
| [7] | 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 |
| [8] | 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 |
| [9] | Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem-proving, Commun. ACM, 5, 394-397 (1962) · Zbl 0217.54002 |
| [10] | Giunchiglia, E.; Narizzano, M.; Tacchella, A., Clause/term resolution and learning in the evaluation of quantified Boolean formulas, J. Artificial Intelligence Res., 26, 371-416 (2006) · Zbl 1183.68475 |
| [11] | Goultiaeva, A.; Gelder, A. V.; Bacchus, F., A uniform approach for generating proofs and strategies for both true and false QBF formulas, (Walsh, T., Proceedings of IJCAI 2011 (2011), IJCAI/AAAI), 546-553 |
| [12] | Heule, M.; Seidl, M.; Biere, A., A unified proof system for QBF preprocessing, (Demri, S.; Kapur, D.; Weidenbach, C., Automated Reasoning, 7th International Joint Conference. Automated Reasoning, 7th International Joint Conference, IJCAR 2014. Automated Reasoning, 7th International Joint Conference. Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Lecture Notes in Computer Science, vol. 8562 (2014), Springer Verlag), 91-106 · Zbl 1409.68257 |
| [13] | Janota, M.; Chew, L.; Beyersdorff, O., On unification of QBF resolution-based calculi, Electron. Colloq. Comput. Complex. (2014) · Zbl 1426.68283 |
| [14] | Janota, M.; Marques-Silva, J., On propositional QBF expansions and Q-resolution, (Järvisalo, M.; Gelder, A. V., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2013. Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2013, Lecture Notes in Computer Science, vol. 7962 (2013), Springer Verlag), 67-82 · Zbl 1390.03017 |
| [15] | Kautz, H.; Selman, B., Pushing the envelope: planning, propositional logic, and stochastic search, (Proceedings of the Thirteenth AAAI Conference on Artificial Intelligence. Proceedings of the Thirteenth AAAI Conference on Artificial Intelligence, AAAI’96 (1996), AAAI Press), 1194-1201 |
| [16] | Lonsing, F., Dependency schemes and search-based qbf solving: theory and practice (Apr. 2012), Johannes Kepler University: Johannes Kepler University Linz, Austria, PhD thesis |
| [17] | Prasad, A. G.M.; Biere, A., A survey of recent advances in SAT-based formal verification, Softw. Tools Technol. Transf., 7, 2, 156-173 (2005) |
| [18] | Niemetz, A.; Preiner, M.; Lonsing, F.; Seidl, M.; Biere, A., Resolution-based certificate extraction for QBF, (Cimatti, A.; Sebastiani, R., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2012. Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2012, Lecture Notes in Computer Science, vol. 7317 (2012), Springer Verlag), 430-435 |
| [19] | Peterson, G.; Reif, J.; Azhar, S., Lower bounds for multiplayer noncooperative games of incomplete information, Comput. Math. Appl., 41, 78, 957-992 (2001) · Zbl 0991.91007 |
| [20] | Samer, M., Variable dependencies of quantified CSPs, (Cervesato, I.; Veith, H.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 15th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 15th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Lecture Notes in Computer Science, vol. 5330 (2008), Springer Verlag), 512-527 · Zbl 1182.68268 |
| [21] | Samer, M.; Szeider, S., Backdoor sets of quantified Boolean formulas, J. Automat. Reason., 42, 1, 77-97 (2009) · Zbl 1191.68353 |
| [22] | Silva, J. P.M., The impact of branching heuristics in propositional satisfiability algorithms, (Barahona, P.; Alferes, J. J., Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence. Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence, EPIA ’99. Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence. Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence, EPIA ’99, Lecture Notes in Computer Science, vol. 1695 (1999), Springer Verlag), 62-74 |
| [23] | Slivovsky, F.; Szeider, S., Computing resolution-path dependencies in linear time, (Cimatti, A.; Sebastiani, R., Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2012. Theory and Applications of Satisfiability Testing. Theory and Applications of Satisfiability Testing, SAT 2012, Lecture Notes in Computer Science, vol. 7317 (2012), Springer Verlag), 58-71 · Zbl 1273.68187 |
| [24] | Van Gelder, A., Variable independence and resolution paths for quantified Boolean formulas, (Lee, J., Principles and Practice of Constraint Programming. Principles and Practice of Constraint Programming, CP 2011. Principles and Practice of Constraint Programming. Principles and Practice of Constraint Programming, CP 2011, Lecture Notes in Computer Science, vol. 6876 (2011), Springer Verlag), 789-803 · Zbl 1273.68188 |
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.
