Document Open Access Logo

Are Short Proofs Narrow? QBF Resolution is not Simple

Authors Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla

PDF

File

Thumbnail PDF
PDF
LIPIcs.STACS.2016.15.pdf
  • Filesize: 0.68 MB
  • 14 pages

Document Identifiers

Subject Classification

Keywords
  • proof complexity
  • QBF
  • resolution
  • lower bound techniques
  • simulations

Metrics

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

Abstract

The groundbreaking paper 'Short proofs are narrow - resolution made simple' by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that space lower bounds again can be obtained via width lower bounds. 

Here we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBF). A mixed picture emerges. Our main results show that both the relations between size and width as well as between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems Forall-Exp+Res and IR-calc, however only in the weak tree-like models. 

Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results we exhibit space and width-preserving simulations between QBF resolution calculi.

Cite As Get BibTex

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are Short Proofs Narrow? QBF Resolution is not Simple. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.STACS.2016.15

Author Details

Olaf Beyersdorff
Leroy Chew
Meena Mahajan
Anil Shukla

References

  1. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008. Google Scholar
  2. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Form. Methods Syst. Des., 41(1):45-65, August 2012. Google Scholar
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Proc. Theory and Applications of Satisfiability Testing (SAT'14), pages 154-169, 2014. Google Scholar
  4. Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In Proc. ACM Symposium on Theory of Computing (STOC'12), pages 213-232, 2012. Google Scholar
  5. Eli Ben-Sasson. Size space tradeoffs for resolution. In Proc. Annual ACM Symposium on Theory of Computing (STOC'02), pages 457-464, 2002. Google Scholar
  6. Eli Ben-Sasson and Jakob Nordström. Understanding space in proof complexity: Separations and trade-offs via substitutions. In Proc. Innovations in Computer Science (ICS'11), pages 401-416, 2011. Google Scholar
  7. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Google Scholar
  8. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. JSAT, 5(1-4):133-191, 2008. Google Scholar
  9. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: from circuits to QBF proof systems. In Proc. Innovations in Theoretical Computer Science (ITCS'16), 2016. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In Proc. Mathematical Foundations of Computer Science (MFCS'14), pages 81-93, 2014. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. Proof complexity of resolution-based QBF calculi. In Proc. Symposium on Theoretical Aspects of Computer Science(STACS'15), pages 76-89, 2015. Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. In Proc. Automata, Languages, and Programming - 42nd International Colloquium (ICALP'15), pages 180-192, 2015. Google Scholar
  13. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-resolution size. In Proc. International Conference on Language and Automata Theory and Applications(LATA'15), pages 486-498, 2015. Google Scholar
  14. Olaf Beyersdorff and Oliver Kullmann. Unified characterisations of resolution hardness measures. In Proc. Theory and Applications of Satisfiability Testing (SAT'14), pages 170-187, 2014. Google Scholar
  15. Archie Blake. Canonical expressions in boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  16. Maria Luisa Bonet and Nicola Galesi. A study of proof search algorithms for resolution and polynomial calculus. In Proc. Annual Symposium on Foundations of Computer Science (FOCS'99), 1999. Google Scholar
  17. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. In Proc. Artificial Intelligence and Symbolic Computation (AISC'14), pages 120-131, 2014. Google Scholar
  18. Juan Luis Esteban and Jacobo Torán. Space bounds for resolution. Information and Computation, 171(1):84-97, 2001. Google Scholar
  19. Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, and Marc Vinyals. From small space to small width in resolution. In International Symposium on Theoretical Aspects of Computer Science (STACS'14), pages 300-311, 2014. Google Scholar
  20. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  21. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  22. Jan Krajíček. Interpolation theorems, lower bounds for proof systems and independence results for bounded arithmetic. Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  23. Oliver Kullmann. Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Electronic Colloquium on Computational Complexity (ECCC), 99(41), 1999. Google Scholar
  24. Jakob Nordström. Pebble games, proof complexity, and time-space trade-offs. Logical Methods in Computer Science, 9(3), 2013. Google Scholar
  25. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In AAAI, pages 1045-1050. AAAI Press, 2007. Google Scholar
  26. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23-41, 1965. Google Scholar
  27. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Proc. Principles and Practice of Constraint Programming (CP'12), pages 647-663, 2012. Google Scholar
  28. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified boolean satisfiability solver. In Proc. IEEE/ACM International Conference on Computer-aided Design (ICCAD'02), 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact