Long-Distance Q-Resolution with Dependency Schemes
Tóm tắt
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers that use these systems to generate proofs. We study a combination of two proof systems supported by the solver DepQBF: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system—which we call long-distance Q(D)-resolution—is sound for the reflexive resolution-path dependency scheme. In fact, we prove that it admits strategy extraction in polynomial time. This comes as an application of a general result, by which we identify a whole class of dependency schemes for which long-distance Q(D)-resolution admits polynomial-time strategy extraction. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q(D)-resolution with the standard dependency scheme. We further show that search-based QBF solvers using a dependency scheme D and learning with long-distance Q-resolution generate long-distance Q(D)-resolution proofs. The above soundness results thus translate to partial soundness results for such solvers: they declare an input QBF to be false only if it is indeed false. Finally, we report on experiments with a configuration of DepQBF that uses the standard dependency scheme and learning based on long-distance Q-resolution.
Tài liệu tham khảo
Arora, S., Barak, B.: Computational Complexity–A Modern Approach. Cambridge University Press, Cambridge (2009)
Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)
Balabanov, V., Jiang, J.R., Janota, M., Widl, M.: Efficient extraction of QBF (counter) models from long-distance resolution proofs. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, AAAI 2015, pp. 3694–3701. AAAI Press (2015)
Balabanov, V., Widl, M., Jiang, J.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) Theory and Applications of Satisfiability Testing–SAT 2014, Lecture Notes in Computer Science, vol. 8561, pp. 154–169. Springer, Berlin (2014)
Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisf. Boolean Model. Comput. 5(1–4), 133–191 (2008)
Beyersdorff, O., Blinkhorn, J.: Dependency schemes in QBF calculi: semantics and soundness. In: Rueher, M. (ed.) Principles and Practice of Constraint Programming-22nd International Conference, CP 2016, Lecture Notes in Computer Science, vol. 9892, pp. 96–112. Springer, Berlin (2016)
Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M. Ésik, Z. (eds.) Mathematical Foundations of Computer Science 2014–39th International Symposium, MFCS 2014, Lecture Notes in Computer Science, vol. 8635, pp. 81–93. Springer, Berlin (2014)
Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Mayr, E.W., Ollinger, N. (eds.) 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik (2015)
Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Feasible interpolation for QBF resolution calculi. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) Automata, Languages, and Programming–42nd International Colloquium, ICALP 2015, Lecture Notes in Computer Science, vol. 9134, pp. 180–192. Springer, Berlin (2015)
Biere, A., Lonsing, F.: Integrating dependency schemes in search-based QBF solvers. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing–SAT 2010, Lecture Notes in Computer Science, vol. 6175, pp. 158–171. Springer, Berlin (2010)
Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) International Conference on Automated Deduction–CADE 23, Lecture Notes in Computer Science, vol. 6803, pp. 101–115. Springer, Berlin (2011)
Blinkhorn, J., Beyersdorff, O.: Shortening QBF proofs with dependency schemes. In: Theory and Applications of Satisfiability Testing–SAT 2017, Lecture Notes in Computer Science, vol. 10491, pp. 263–280. Springer, Berlin (2017)
Bloem, R., Könighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation–VMCAI 2014, Lecture Notes in Computer Science, vol. 8318, pp. 1–20. Springer, Berlin (2014)
Bubeck, U.: Model-based transformations for quantified Boolean formulas. Ph.D. thesis, University of Paderborn (2010)
Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate Quantified Boolean Formulae and its experimental evaluation. J. Autom. Reason. 28(2), 101–142 (2002)
Cashmore, M., Fox, M., Giunchiglia, E.: Partially grounded planning as Quantified Boolean Formula. In: Borrajo, D., Kambhampati, S., Oddi, A., Fratini, S. (eds.) 23rd International Conference on Automated Planning and Scheduling, ICAPS 2013. AAAI (2013)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5, 394–397 (1962)
Egly, U.: On sequent systems and resolution for QBFs. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing–SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 100–113. Springer, Berlin (2012)
Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning–LPAR 2013, Lecture Notes in Computer Science, vol. 8312, pp. 291–308. Springer, Berlin (2013)
Gelder, A.V.: Contributions to the theory of practical quantified boolean formula solving. In: Milano, M. (ed.) Principles and Practice of Constraint Programming–18th International Conference, CP 2012, Lecture Notes in Computer Science, vol. 7514, pp. 647–663. Springer, Berlin (2012)
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)
Goultiaeva, A., Bacchus, F.: Exploiting QBF duality on a circuit representation. In: Fox, M., Poole, D. (eds.) Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010. AAAI Press (2010)
Goultiaeva, A., Seidl, M., Biere, A.: Bridging the gap between dual propagation and CNF-based QBF solving. In: Macii, E. (ed.) Design, Automation and Test in Europe, DATE 13, pp. 811–814. EDA Consortium San Jose, CA, USA/ACM DL (2013)
Goultiaeva, A., Van Gelder, A., Bacchus, F.: A uniform approach for generating proofs and strategies for both true and false QBF formulas. In: Walsh, T. (ed.) Proceedings of IJCAI 2011, pp. 546–553. IJCAI/AAAI (2011)
Heule, M., Seidl, M., Biere, A.: A unified proof system for QBF preprocessing. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning–7th International Joint Conference, IJCAR 2014, Lecture Notes in Computer Science, vol. 8562, pp. 91–106. Springer, Berlin (2014)
Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.M.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing–SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 114–128. Springer, Berlin (2012)
Janota, M., Marques-Silva, J.: On propositional QBF expansions and Q-resolution. In: Järvisalo, M., Van Gelder, A. (eds.) Theory and Applications of Satisfiability Testing–SAT 2013, Lecture Notes in Computer Science, vol. 7962, pp. 67–82. Springer, Berlin (2013)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)
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.) Theory and Applications of Satisfiability Testing–SAT 2010, Lecture Notes in Computer Science, vol. 6175, pp. 128–142. Springer, Berlin (2010)
Kronegger, M., Pfandler, A., Pichler, R.: Conformant planning as benchmark for QBF-solvers. In: International Workshop on Quantified Boolean Formulas–QBF 2013 (2013). http://fmv.jku.at/qbf2013/
Lonsing, F.: Dependency schemes and search-based QBF solving: theory and practice. Ph.D. thesis, Johannes Kepler University, Linz, Austria (2012)
Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning-20th International Conference, LPAR-20 2015. Lecture Notes in Computer Science, vol. 9450, pp. 418–433. Springer, Berlin (2015)
Lonsing, F., Egly, U., Van Gelder, A.: Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In: Järvisalo, M., Van Gelder, A. (eds.) Theory and Applications of Satisfiability Testing–SAT 2013, Lecture Notes in Computer Science, vol. 7962, pp. 100–115. Springer, Berlin (2013)
Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence, EPIA ’99, Lecture Notes in Computer Science, vol. 1695, pp. 62–74. Springer, Berlin (1999)
Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing–SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 430–435. Springer, Berlin (2012)
Peitl, T., Slivovsky, F., Szeider, S.: Long distance Q-resolution with dependency schemes. In: Creignou, N., Berre, D.L. (eds.) Theory and Applications of Satisfiability Testing–SAT 2016, Lecture Notes in Computer Science, vol. 9710, pp. 500–518. Springer, Berlin (2016)
Peitl, T., Slivovsky, F., Szeider, S.: Dependency learning for QBF. In: Gaspers, S., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing–SAT 2017, Lecture Notes in Computer Science, vol. 10491, pp. 298–313. Springer, Berlin(2017)
Rintanen, J.: Asymptotically optimal encodings of conformant planning in QBF. In: 22nd AAAI Conference on Artificial Intelligence, AAAI 2007, pp. 1045–1050. AAAI (2007)
Samer, M., Szeider, S.: Backdoor sets of quantified Boolean formulas. J. Autom. Reason. 42(1), 77–97 (2009)
Slivovsky, F.: Structure in #SAT and QBF. Ph.D. thesis, TU Wien (2015)
Slivovsky, F., Szeider, S.: Computing resolution-path dependencies in linear time. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing–SAT 2012, Lecture Notes in Computer Science, vol. 7317, pp. 58–71. Springer, Berlin (2012)
Slivovsky, F., Szeider, S.: Soundness of Q-resolution with dependency schemes. Theoret. Comput. Sci. 612, 83–101 (2016)
Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) Theory and Applications of Satisfiability Testing–SAT 2007, Lecture Notes in Computer Science, vol. 4501, pp. 355–368. Springer, Berlin(2007)
Van Gelder, A.: Variable independence and resolution paths for quantified Boolean formulas. In: Lee, J. (ed.) Principles and Practice of Constraint Programming–CP 2011, Lecture Notes in Computer Science, vol. 6876, pp. 789–803. Springer, Berlin (2011)
Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Pileggi, L.T. Kuehlmann, A. (eds.) Proceedings of the 2002 IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, pp. 442–449. ACM/IEEE Computer Society (2002)
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Brinksma, D., Larsen, K.G. (eds.) Computer Aided Verification: 14th International Conference (CAV 2002), Lecture Notes in Computer Science, vol. 2404, pp. 17–36 (2002)
Zhang, L., Malik, S.: Towards a symmetric treatment of satisfaction and conflicts in quantified Boolean formula evaluation. In: Hentenryck, P.V. (ed.) Principles and Practice of Constraint Programming–8th International Conference, CP 2002, Lecture Notes in Computer Science, vol. 2470, pp. 200–215. Springer, Berlin (2002)