Document Open Access Logo

Understanding Cutting Planes for QBFs

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2016.40.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • proof complexity
  • QBF
  • cutting planes
  • resolution
  • simulations

Metrics

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

Abstract

We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res.

Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.

Cite As Get BibTex

Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding Cutting Planes for QBFs. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 40:1-40:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.40

Author Details

Olaf Beyersdorff
Leroy Chew
Meena Mahajan
Anil Shukla

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. URL: http://dx.doi.org/10.1016/j.jcss.2014.04.014.
  3. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45-65, 2012. URL: http://dx.doi.org/10.1007/s10703-012-0152-6.
  4. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In SAT'14, pages 154-169, 2014. Google Scholar
  5. Marco Benedetti and Hratch Mangassarian. QBF-based formal verification: Experience and perspectives. JSAT, 5(1-4):133-191, 2008. Google Scholar
  6. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Proc. ACM Conference on Innovations in Theoretical Computer Science (ITCS'16), pages 249-260. ACM, 2016. Google Scholar
  7. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In MFCS, II, pages 81-93, 2014. Google Scholar
  8. 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. LIPIcs, 2015. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. In Proc. International Colloquium on Automata, Languages, and Programming (ICALP'15), pages 180-192. Springer, 2015. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not simple. In Proc. Symposium on Theoretical Aspects of Computer Science (STACS'16), 2016. Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-resolution size. In LATA, pages 486-498. Springer, 2015. Google Scholar
  12. Olaf Beyersdorff and Ján Pich. Understanding Gentzen and Frege systems for QBF. In Proc. ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016. Google Scholar
  13. A. Blake. Canonical expressions in boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  14. Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-automatizability of bounded-depth Frege proofs. Computational Complexity, 13(1-2):47-68, 2004. Google Scholar
  15. Samuel R. Buss. Polynomial size proofs of the propositional pigeonhole principle. J. Symb. Log., 52(4):916-927, 1987. Google Scholar
  16. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  17. Václav Chvátal. Edmonds polytopes and weakly hamiltonian graphs. Math. Program., 5(1):29-40, 1973. Google Scholar
  18. 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
  19. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. Google Scholar
  20. Uwe Egly. On sequent systems and resolution for QBFs. In Theory and Applications of Satisfiability Testing (SAT'12), pages 100-113, 2012. Google Scholar
  21. Uwe Egly, Martin Kronegger, Florian Lonsing, and Andreas Pfandler. Conformant planning as a case study of incremental QBF solving. In Artificial Intelligence and Symbolic Computation (AISC'14), pages 120-131, 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 Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference (LPAR), pages 291-308, 2013. Google Scholar
  23. Yuval Filmus, Pavel Hrubes, and Massimo Lauria. Semantic versus syntactic cutting planes. In 33rd Symposium on Theoretical Aspects of Computer Science, STACS , Orléans, France, pages 35:1-35:13, 2016. Google Scholar
  24. Andreas Goerdt. Cutting plane versus Frege proof systems. In Computer Science Logic, 4th Workshop, CSL'90, Heidelberg, Germany, October 1-5, Proceedings, pages 174-194, 1990. Google Scholar
  25. Ralph E. Gomory. Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society, 64(5):275–278, 1958. Google Scholar
  26. Alexandra Goultiaeva, Allen Van Gelder, and Fahiem Bacchus. A uniform approach for generating proofs and strategies for both true and false QBF formulas. In IJCAI, pages 546-553, 2011. Google Scholar
  27. Amin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  28. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  29. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  30. 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
  31. Jan Krajíček and Pavel Pudlák. Some consequences of cryptographical conjectures for S¹₂ and EF. Information and Computation, 140(1):82-94, 1998. Google Scholar
  32. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994. Google Scholar
  33. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. Google Scholar
  34. Jussi Rintanen. Asymptotically optimal encodings of conformant planning in QBF. In AAAI, pages 1045-1050. AAAI Press, 2007. Google Scholar
  35. Ronald L. Rivest. Learning decision lists. Machine Learning, 2(3):229-246, 1987. Google Scholar
  36. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23-41, 1965. Google Scholar
  37. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  38. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In CP, pages 647-663, 2012. Google Scholar
  39. Heribert Vollmer. Introduction to Circuit Complexity - A Uniform Approach. Texts in Theoretical Computer Science. Springer Verlag, Berlin Heidelberg, 1999. 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