Document Open Access Logo

Lower Bound Techniques for QBF Proof Systems

Author Meena Mahajan

PDF
Thumbnail PDF

File

LIPIcs.STACS.2018.2.pdf
  • Filesize: 436 kB
  • 8 pages

Document Identifiers

Author Details

Meena Mahajan

Cite As Get BibTex

Meena Mahajan. Lower Bound Techniques for QBF Proof Systems. In 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 96, pp. 2:1-2:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.STACS.2018.2

Abstract

How do we prove that a false QBF is inded false? How big a proof is needed?  The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended - in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent
genuine QBF lower bounds based on a semantic cost measure.

This talk will provide a broad overview of some of these developments.

Subject Classification

Keywords
  • Proof Complexity
  • Quantified Boolean formulas
  • Resolution
  • Lower Bound Techniques

Metrics

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

References

  1. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. URL: https://doi.org/10.1016/j.jcss.2007.06.025, URL: http://dx.doi.org/10.1016/j.jcss.2007.06.025.
  2. 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
  3. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Proceeding of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 154-169, 2014. Google Scholar
  4. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, 2001. Google Scholar
  5. Olaf Beyersdorff and Joshua Blinkhorn. Genuine lower bounds for QBF expansion. In Proceedings of the 35th Symposium on Theoretical Aspects of Computer Science (STACS), page to appear, 2018. Google Scholar
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. In Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS), page to appear, 2018. Google Scholar
  7. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In Proceedings of the ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 249-260. ACM, 2016. Google Scholar
  8. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. On unification of QBF resolution-based calculi. In Proceedings of 39th International Symposium on Mathematical Foundations of Computer Science MFCS, Proceedings Part II, LNCS 8635, pages 81-93, 2014. Google Scholar
  9. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. Proof complexity of resolution-based QBF calculi. In Proceedings of the 32nd International Symposium on Theoretical Aspects of Computer Science (STACS), pages 76-89. LIPIcs, 2015. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Are short proofs narrow? QBF resolution is not so simple. ACM Transactions on Computational Logic, 19(1):1:1-1:26, Dec 2017. (preliminary version in STACS 2016). Google Scholar
  11. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible Interpolation for QBF Resolution Calculi. Logical Methods in Computer Science, Volume 13, Issue 2, 2017. (preliminary version in ICALP 2015). Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. Electronic Colloquium on Computational Complexity (ECCC), 24:37, 2017. (preliminary version in FSTTCS 2016). Google Scholar
  13. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016), pages 14:1-14:14, 2017. Google Scholar
  14. Olaf Beyersdorff and Ján Pich. Understanding Gentzen and Frege systems for QBF. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 146-155, 2016. Google Scholar
  15. Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate Quantified Boolean Formulae. In Proceedings of the 15th National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference (AAAI), pages 262-267, 1998. Google Scholar
  16. Marco Cadoli, Marco Schaerf, Andrea Giovanardi, and Massimo Giovanardi. An algorithm to evaluate Quantified Boolean Formulae and its experimental evaluation. Journal of Automated Reasoning, 28(2):101-142, 2002. Google Scholar
  17. Leroy Chew. QBF Proof Complexity. PhD thesis, University of Leeds, UK, 2017. Google Scholar
  18. Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752-794, 2003. Google Scholar
  19. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 291-308. Springer Berlin Heidelberg, 2013. Google Scholar
  20. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. QuBE++: An efficient QBF solver. In Formal Methods in Computer-Aided Design, pages 201-213. Springer Berlin Heidelberg, 2004. Google Scholar
  21. Mikolás Janota, William Klieber, João Marques-Silva, and Edmund M. Clarke. Solving QBF with counterexample guided refinement. In Proceeding of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 114-128, 2012. Google Scholar
  22. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015. Google Scholar
  23. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Information and Computation, 117(1):12-18, 1995. Google Scholar
  24. William Klieber, Samir Sapra, Sicun Gao, and Edmund M. Clarke. A non-prenex, non-clausal QBF solver with game-state learning. In 13th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 128-142, 2010. Google Scholar
  25. 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
  26. Pavel Pudlák. Lower bounds for resolution and cutting planes proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  27. Markus N. Rabe and Leander Tentrup. CAQE: A certifying QBF solver. In Formal Methods in Computer-Aided Design, (FMCAD), pages 136-143, 2015. Google Scholar
  28. Anil Shukla. On Proof Complexity for Quantified Boolean Formulas. PhD thesis, The Institute of Mathematical Sciences, HBNI, India, 2017. Google Scholar
  29. György Turán and Farrokh Vatan. Linear decision lists and partitioning algorithms for the construction of neural networks. In Foundations of Computational Mathematics. Springer, 1997. Google Scholar
  30. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP), pages 647-663, 2012. Google Scholar
  31. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In International Conference on Computer Aided Design, 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 About DROPS Imprint Privacy Contact