Document Open Access Logo

Proof Complexity of Resolution-based QBF Calculi

Authors Olaf Beyersdorff, Leroy Chew, Mikolás Janota

PDF
Thumbnail PDF

File

LIPIcs.STACS.2015.76.pdf
  • Filesize: 0.72 MB
  • 14 pages

Document Identifiers

Author Details

Olaf Beyersdorff
Leroy Chew
Mikolás Janota

Cite AsGet BibTex

Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. Proof Complexity of Resolution-based QBF Calculi. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 76-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.STACS.2015.76

Abstract

Proof systems for quantified Boolean formulas (QBFs) provide a theoretical underpinning for the performance of important QBF solvers. However, the proof complexity of these proof systems is currently not well understood and in particular lower bound techniques are missing. In this paper we exhibit a new and elegant proof technique for showing lower bounds in QBF proof systems based on strategy extraction. This technique provides a direct transfer of circuit lower bounds to lengths of proofs lower bounds. We use our method to show the hardness of a natural class of parity formulas for Q-resolution and universal Q-resolution. Variants of the formulas are hard for even stronger systems as long-distance Q-resolution and extensions. With a completely different lower bound argument we show the hardness of the prominent formulas of Kleine Büning et al. [34] for the strong expansion-based calculus IR-calc. Our lower bounds imply new exponential separations between two different types of resolution-based QBF calculi: proof systems for CDCL-based solvers (Q-resolution, long-distance Q-resolution) and proof systems for expansion-based solvers (forallExp+Res and its generalizations IR-calc and IRM-calc). The relations between proof systems from the two different classes were not known before.
Keywords
  • proof complexity
  • QBF
  • lower bound techniques
  • separations

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009. Google Scholar
  2. Albert Atserias and Sergi Oliva. Bounded-width QBF is PSPACE-complete. J. Comput. Syst. Sci., 80(7):1415-1429, 2014. Google Scholar
  3. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45-65, 2012. Google Scholar
  4. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Sinz and Egly [41], pages 154-169. Google Scholar
  5. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In SAT, pages 154-169, 2014. Google Scholar
  6. Marco Benedetti. Evaluating QBFs via symbolic Skolemization. In Franz Baader and Andrei Voronkov, editors, LPAR, volume 3452, pages 285-300. Springer, 2004. Google Scholar
  7. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. JSAT, 5(1-4):133-191, 2008. Google Scholar
  8. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In MFCS, II, pages 81-93, 2014. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-resolution size. In LATA. Springer, 2015. Google Scholar
  10. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A lower bound for the pigeonhole principle in tree-like resolution by asymmetric prover-delayer games. Information Processing Letters, 110(23):1074-1077, 2010. Google Scholar
  11. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A characterization of tree-like resolution size. Information Processing Letters, 113(18):666-671, 2013. Google Scholar
  12. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Parameterized complexity of DPLL search procedures. ACM Transactions on Computational Logic, 14(3), 2013. Google Scholar
  13. Olaf Beyersdorff and Sebastian Müller. A tight Karp-Lipton collapse result in bounded arithmetic. ACM Transactions on Computational Logic, 11(4), 2010. Google Scholar
  14. Armin Biere. Resolve and expand. In SAT, pages 238-246, 2004. Google Scholar
  15. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. Google Scholar
  16. Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, and Jan Johannsen. On the relative complexity of resolution refinements and cutting planes proof systems. SIAM J. Comput., 30(5):1462-1484, 2000. Google Scholar
  17. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  18. Jin-Yi Cai. S₂^p ⊆ ZPP^NP. Journal of Computer and System Sciences, 73(1):25-35, 2007. Google Scholar
  19. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  20. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  21. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. CoRR, abs/1405.7253, 2014. Google Scholar
  22. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In McMillan et al. [36], pages 291-308. Google Scholar
  23. Merrick L. Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. Mathematical Systems Theory, 17(1):13-27, 1984. Google Scholar
  24. Enrico Giunchiglia, Paolo Marin, and Massimo Narizzano. Reasoning with quantified boolean formulas. In Biere et al. [15], pages 761-780. Google Scholar
  25. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In Toby Walsh, editor, IJCAI, pages 546-553. IJCAI/AAAI, 2011. Google Scholar
  26. Johan Håstad. Computational Limitations of Small-depth Circuits. MIT Press, Cambridge, MA, USA, 1987. Google Scholar
  27. Marijn Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In Automated Reasoning - 7th International Joint Conference, IJCAR, volume 8562, pages 91-106. Springer, 2014. Google Scholar
  28. Mikoláš Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In Alessandro Cimatti and Roberto Sebastiani, editors, SAT, volume 7317, pages 114-128. Springer, 2012. Google Scholar
  29. Mikoláš Janota, Radu Grigore, and Joao Marques-Silva. On QBF proofs and preprocessing. In McMillan et al. [36], pages 473-489. Google Scholar
  30. Mikoláš Janota and Joao Marques-Silva. ∀Exp+Res does not P-Simulate Q-resolution. International Workshop on Quantified Boolean Formulas, 2013. Google Scholar
  31. Mikoláš Janota and Joao Marques-Silva. On propositional QBF expansions and Q-resolution. In M. Järvisalo and A. Van Gelder, editors, SAT, pages 67-82. Springer, 2013. Google Scholar
  32. Richard M. Karp and Richard J. Lipton. Some connections between nonuniform and uniform complexity classes. In Proc. 12th ACM Symposium on Theory of Computing, pages 302-309. ACM Press, 1980. Google Scholar
  33. Hans Kleine Büning and Uwe Bubeck. Theory of quantified boolean formulas. In Biere et al. [15], pages 735-760. Google Scholar
  34. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  35. Jan Krajíček. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  36. Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors. Logic for Programming, Artificial Intelligence, and Reasoning, LPAR. Springer, 2013. Google Scholar
  37. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  38. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In AAAI, pages 1045-1050. AAAI Press, 2007. Google Scholar
  39. Ronald L. Rivest. Learning decision lists. Machine Learning, 2(3):229-246, 1987. Google Scholar
  40. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  41. Carsten Sinz and Uwe Egly, editors. Theory and Applications of Satisfiability Testing - SAT, volume 8561. Springer, 2014. Google Scholar
  42. Friedrich Slivovsky and Stefan Szeider. Variable dependencies and Q-resolution. In Sinz and Egly [41], pages 269-284. Google Scholar
  43. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Michela Milano, editor, CP, volume 7514, pages 647-663. Springer, 2012. Google Scholar
  44. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In ICCAD, pages 442-449, 2002. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact