Reinterpreting dependency schemes: soundness meets incompleteness in DQBF. (English) Zbl 1468.03008
Summary: Dependency quantified Boolean formulas (DQBF) and QBF dependency schemes have been treated separately in the literature, even though both treatments extend QBF by replacing the linear order of the quantifier prefix with a partial order. We propose to merge the two, by reinterpreting a dependency scheme as a mapping from QBF into DQBF. Our approach offers a fresh insight on the nature of soundness in proof systems for QBF with dependency schemes, in which a natural property called “full exhibition” is central. We apply our approach to QBF proof systems from two distinct paradigms, termed “universal reduction” and “universal expansion”. We show that full exhibition is sufficient (but not necessary) for soundness in universal reduction systems for QBF with dependency schemes, whereas for expansion systems the same property characterises soundness exactly. We prove our results by investigating DQBF proof systems, and then employing our reinterpretation of dependency schemes. Finally, we show that the reflexive resolution path dependency scheme is fully exhibited, thereby proving a conjecture of Slivovsky.
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] | Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, 2 volumes, pp. 19-99. Elsevier and MIT Press (2001) · Zbl 0993.03008 |
| [3] | Balabanov, V., Chiang, H.K., Jiang, J.R.: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF. Theor. Comput. Sci. 523, 86-100 (2014) · Zbl 1283.03032 · doi:10.1016/j.tcs.2013.12.020 |
| [4] | Balabanov, V., Widl, M., Jiang, J.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 8561, pp. 154-169. Springer (2014) · Zbl 1423.68406 |
| [5] | Bayardo Jr., R.J., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) National Conference on Artificial Intelligence (AAAI), pp. 203-208. AAAI Press / The MIT Press (1997) |
| [6] | Beyersdorff, O., Blinkhorn, J.: Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 9892, pp. 96-112. Springer (2016) |
| [7] | Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) International Symposium on Mathematical Foundations of Computer Science (MFCS). Lecture Notes in Computer Science, vol. 8635, pp. 81-93. Springer (2014) · Zbl 1426.68283 |
| [8] | Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) International Symposium on Theoretical Aspects of Computer Science (STACS). Leibniz International Proceedings in Informatics (LIPIcs), vol. 30, pp. 76-89. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015) · Zbl 1355.68105 |
| [9] | Beyersdorff, O., Chew, L., Schmidt, R.A., Suda, M.: Lifting QBF resolution calculi to DQBF. In: Creignou and Berre [16], pp. 490-499 · Zbl 1475.68431 |
| [10] | Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009) · Zbl 1183.68568 |
| [11] | Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Gaspers and Walsh [18], pp. 263-280 · Zbl 1496.68364 |
| [12] | Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 8318, pp. 1-20. Springer (2014) · Zbl 1428.68040 |
| [13] | Bubeck, U., Kleine Büning, H.: Dependency quantified horn formulas: models and complexity. In: Biere, A., Gomes, C.P. (eds.) International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 4121, pp. 198-211. Springer (2006) · Zbl 1187.68256 |
| [14] | Cook, S.A.: The complexity of theorem-proving procedures. In: Harrison, M.A., Banerji, R.B., Ullman, J.D. (eds.) ACM Symposium on Theory of Computing (STOC), pp. 151-158. ACM (1971) · Zbl 0253.68020 |
| [15] | Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36-50 (1979) · Zbl 0408.03044 · doi:10.2307/2273702 |
| [16] | Creignou, N., Berre, D.L. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 9710. Springer (2016) · Zbl 1337.68009 |
| [17] | Fröhlich, A., Kovásznai, G., Biere, A., Veith, H.: iDQ: instantiation-based DQBF solving. In: Berre, D.L. (ed.) Workshop on Pragmatics of SAT (POS), EPiC Series in Computing, vol. 27, pp. 103-116. EasyChair, (2014) |
| [18] | Gaspers, S., Walsh, T. (eds.): International Conference on Theory and Practice of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 10491. Springer (2017) · Zbl 1368.68008 |
| [19] | Gelder, A.V.: Contributions to the theory of practical quantified Boolean formula solving. In: Milano, M. (ed.) International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 7514, pp. 647-663. Springer (2012) · Zbl 1390.68585 |
| [20] | 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 & Exhibition (DATE), pp. 1617-1622. ACM (2015) |
| [21] | Henkin, L.: Some remarks on infinitely long formulas. In Infinistic Methods, pp 167-183. Pergamon Press, Oxford (1961) · Zbl 0121.25308 |
| [22] | Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1-25 (2016) · Zbl 1351.68254 · doi:10.1016/j.artint.2016.01.004 |
| [23] | 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 |
| [24] | Kleine Büning, H., 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 |
| [25] | Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317-353 (1980). https://doi.org/10.1016/0022-0000(80)90027-6 · Zbl 0471.03034 · doi:10.1016/0022-0000(80)90027-6 |
| [26] | Lonsing, F.: Dependency schemes and search-based qbf solving: Theory and practice. Ph.D. thesis, Johannes Kepler University (2012) |
| [27] | Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisf. Boolean Model. Comput. 7(2-3), 71-76 (2010) |
| [28] | Meel, K.S., Vardi, M.Y., Chakraborty, S., Fremont, D.J., Seshia, S.A., Fried, D., Ivrii, A., Malik, S.: Constrained sampling and counting: Universal hashing meets SAT solving. In: Darwiche, A. (ed.) Beyond NP, AAAI Workshops, vol. WS-16-05. AAAI Press (2016) |
| [29] | Rabe, M.N.: A resolution-style proof system for DQBF. In: Gaspers and Walsh [18], pp. 314-325 · Zbl 1496.03050 |
| [30] | Samer, M.: Variable dependencies of quantified CSPs. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Lecture Notes in Computer Science, vol. 5330, pp. 512-527. Springer (2008) · Zbl 1182.68268 |
| [31] | Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77-97 (2009) · Zbl 1191.68353 · doi:10.1007/s10817-008-9114-5 |
| [32] | Samulowitz, H., Bacchus, F.: Using SAT in QBF. In: van Beek, P. (ed.) International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 3709, pp. 578-592. Springer (2005) · Zbl 1153.68485 |
| [33] | Seidl, M., Lonsing, F., Biere, A.: qbf2epr: A tool for generating EPR formulas from QBF. In: Fontaine, P., Schmidt, R.A., Schulz, S. (eds.) Workshop on Practical Aspects of Automated Reasoning PAAR, EPiC Series in Computing, vol. 21, pp. 139-148. EasyChair (2012) |
| [34] | Silva, J.P.M., Sakallah, K.A.: GRASP-a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) International Conference on Computer-Aided Design (ICCAD), pp. 220-227. IEEE Computer Society/ACM (1996) |
| [35] | Slivovsky, F.: Structure in \[\#\]#SAT and QBF. Ph.D. thesis, Vienna University of Technology (2015) |
| [36] | Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time. In: Cimatti, A., Sebastiani, R. (eds.) International Conference on Theory and Applications of Satisfiability Testing (SAT). Lecture Notes in Computer Science, vol. 7317, pp. 58-71. Springer (2012) · Zbl 1273.68187 |
| [37] | Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theor. Comput. Sci. 612, 83-101 (2016) · Zbl 1332.68204 · doi:10.1016/j.tcs.2015.10.020 |
| [38] | Stockmeyer, L.J., Meyer, A.R.: Word problems requiring exponential time: preliminary report. In: Aho, A.V., Borodin, A., Constable, R.L., Floyd, R.W., Harrison, M.A., Karp, R.M., Strong, H.R. (eds.) ACM Symposium on Theory of Computing (STOC), pp. 1-9. ACM (1973) · Zbl 0359.68050 |
| [39] | Tentrup, L.: On expansion and resolution in CEGAR based QBF solving. In: Majumdar, R., Kuncak, V. (eds.) International Conference on Computer Aided Verification (CAV). Lecture Notes in Computer Science, vol. 10427, pp. 475-494. Springer (2017) · Zbl 1494.68293 |
| [40] | Van Gelder, A.: Variable independence and resolution paths for quantified Boolean formulas. In: Lee, J.H. (ed.) International Conference on Principles and Practice of Constraint Programming (CP). Lecture Notes in Computer Science, vol. 6876, pp. 789-803. Springer (2011) · Zbl 1273.68188 |
| [41] | Vardi, M.Y.: Boolean satisfiability: theory and engineering. ACM 57(3), 5 (2014) · doi:10.1145/2578043 |
| [42] | Wimmer, R., Scholl, C., Wimmer, K., Becker, B.: Dependency schemes for DQBF. In: Creignou and Berre [16], pp. 473-489 · Zbl 1475.68225 |
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.
