Abstract
Q-resolution is a generalization of propositional resolution that provides the theoretical foundation for search-based solvers of quantified Boolean formulas (QBFs). Recently, it has been shown that an extension of Q-resolution, called long-distance resolution, is remarkably powerful both in theory and in practice. However, it was unknown how long-distance resolution is related to \(\mathsf {QRAT}\), a proof system introduced for certifying the correctness of QBF-preprocessing techniques. We show that \(\mathsf {QRAT}\) polynomially simulates long-distance resolution. Two simple rules of \(\mathsf {QRAT}\) are crucial for our simulation—blocked-literal addition and blocked-literal elimination. Based on the simulation, we implemented a tool that transforms long-distance-resolution proofs into \(\mathsf {QRAT}\) proofs. In a case study, we compare long-distance-resolution proofs of the well-known Kleine Büning formulas with corresponding \(\mathsf {QRAT}\) proofs.
This work has been supported by the Austrian Science Fund (FWF) under projects W1255-N23 and S11408-N23, and by the National Science Foundation (NSF) under grant number CCF-1618574.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Clause deletion was not used in the simulation, but is allowed in the \(\mathsf {QRAT}\) system.
References
Balabanov, V., Jiang, J.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45–65 (2012)
Balabanov, V., Widl, M., Jiang, J.R.: QBF resolution systems and their proof complexities. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 154–169. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_12
Benedetti, M., Mangassarian, H.: QBF-based formal verification: experience and perspectives. J. Satisf. Boolean Model. Comput. (JSAT ) 5(1–4), 133–191 (2008)
Beyersdorff, O., Bonacina, I., Chew, L.: Lower bounds: from circuits to QBF proof systems. In: Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science (ITCS 2016), pp. 249–260. ACM (2016)
Beyersdorff, O., Chew, L., Janota, M.: On unification of QBF resolution-based calculi. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014. LNCS, vol. 8635, pp. 81–93. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44465-8_8
Beyersdorff, O., Chew, L., Janota, M.: Proof complexity of resolution-based QBF calculi. In: Proceedings of the 32nd Internation Symposium on Theoretical Aspects of Computer Science (STACS 2015). LIPIcs, vol. 30, pp. 76–89. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)
Beyersdorff, O., Chew, L., Mahajan, M., Shukla, A.: Are short proofs narrow? QBF resolution is not simple. In: Proceedings of the 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). LIPIcs, vol. 47, pp. 15:1–15:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
Beyersdorff, O., Pich, J.: Understanding Gentzen and Frege systems for QBF. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), pp. 146–155. ACM (2016)
Chen, H.: Proof complexity modulo the polynomial hierarchy: understanding alternation as a source of hardness. In: Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). LIPIcs, vol. 55, pp. 94:1–94:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)
Egly, U.: On stronger calculi for QBFs. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 419–434. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_26
Egly, U., Lonsing, F., Widl, M.: Long-distance resolution: proof generation and strategy extraction in search-based QBF solving. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 291–308. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_21
Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985)
Heule, M.J.H., Hunt Jr., W.A., Wetzler, N.D.: Expressing symmetry breaking in DRAT proofs. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 591–606. Springer, Cham (2015). doi:10.1007/978-3-319-21401-6_40
Heule, M.J.H., Seidl, M., Biere, A.: Blocked literals are universal. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 436–442. Springer, Cham (2015). doi:10.1007/978-3-319-17524-9_33
Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reason. 58(1), 97–125 (2016)
Janota, M.: On Q-resolution and CDCL QBF solving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 402–418. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_25
Janota, M., Grigore, R., Marques-Silva, J.P.: On QBF proofs and preprocessing. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 473–489. Springer, Heidelberg (2013). doi:10.1007/978-3-642-45221-5_32
Janota, M., Klieber, W., Marques-Silva, J.P., Clarke, E.M.: Solving QBF with counterexample guided refinement. Artif. Intell. 234, 1–25 (2016)
Kleine Büning, H., Bubeck, U.: Theory of quantified Boolean formulas. In: Handbook of Satisfiability, pp. 735–760. IOS Press (2009)
Kleine Büning, H., Karpinski, M., Flögel, A.: Resolution for quantified Boolean formulas. Inf. Comput. 117(1), 12–18 (1995)
Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96–97, 149–176 (1999)
Lonsing, F., Egly, U.: DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL. CoRR abs/1702.08256 (2017)
Slivovsky, F., Szeider, S.: Variable dependencies and Q-resolution. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 269–284. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_21
Van Gelder, A.: Contributions to the theory of practical quantified Boolean formula solving. In: Milano, M. (ed.) CP 2012. LNCS, pp. 647–663. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33558-7_47
Wetzler, N.D., Heule, M.J.H., Hunt Jr., W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_31
Zhang, L., Malik, S.: Conflict driven learning in a quantified Boolean satisfiability solver. In: Proceedings of the 2002 IEEE/ACM International Conference on Computer-Aided Design (ICCAD 2002), pp. 442–449. ACM/IEEE Computer Society (2002)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Kiesl, B., Heule, M.J.H., Seidl, M. (2017). A Little Blocked Literal Goes a Long Way. In: Gaspers, S., Walsh, T. (eds) Theory and Applications of Satisfiability Testing – SAT 2017. SAT 2017. Lecture Notes in Computer Science(), vol 10491. Springer, Cham. https://doi.org/10.1007/978-3-319-66263-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-66263-3_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66262-6
Online ISBN: 978-3-319-66263-3
eBook Packages: Computer ScienceComputer Science (R0)