Hard QBFs for Merge Resolution
Document Open Access Logo

Hard QBFs for Merge Resolution

Authors Olaf Beyersdorff , Joshua Blinkhorn , Meena Mahajan , Tomáš Peitl , Gaurav Sood

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2020.12.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Author Details

Olaf Beyersdorff
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Joshua Blinkhorn
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Meena Mahajan
  • The Institute of Mathematical Sciences, HBNI, Chennai, India
Tomáš Peitl
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Gaurav Sood
  • The Institute of Mathematical Sciences, HBNI, Chennai, India

Funding

  • Beyersdorff, Olaf: John Templeton Foundation (grant no. 60842), Carl Zeiss Foundation.
  • Peitl, Tomáš: Grant J-4361 of the Austrian Science Fund FWF.

Acknowledgements

Part of this work was done during the Dagstuhl Seminar "SAT and Interactions" (Seminar 20061).

Cite As Get BibTex

Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomáš Peitl, and Gaurav Sood. Hard QBFs for Merge Resolution. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSTTCS.2020.12

Abstract

We prove the first proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolution systems in the literature, proofs in MRes consist of resolution steps together with information on countermodels, which are syntactically stored in the proofs as merge maps. As demonstrated in [Olaf Beyersdorff et al., 2020], this makes MRes quite powerful: it has strategy extraction by design and allows short proofs for formulas which are hard for classical QBF resolution systems.
Here we show the first exponential lower bounds for MRes, thereby uncovering limitations of MRes. Technically, the results are either transferred from bounds from circuit complexity (for restricted versions of MRes) or directly obtained by combinatorial arguments (for full MRes). Our results imply that the MRes approach is largely orthogonal to other QBF resolution models such as the QCDCL resolution systems QRes and QURes and the expansion systems ∀Exp+Res and IR.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • resolution
  • proof complexity
  • lower bounds

Metrics

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

References

  1. 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
  2. Valeriy Balabanov, Magdalena Widl, and Jie-Hong R. Jiang. QBF resolution systems and their proof complexities. In Carsten Sinz and Uwe Egly, editors, Theory and Applications of Satisfiability Testing - SAT 2014, pages 154-169, Cham, 2014. Springer International Publishing. Google Scholar
  3. Olaf Beyersdorff and Joshua Blinkhorn. Formulas with large weight: a new technique for genuine QBF lower bounds. Electron. Colloquium Comput. Complex., 24:32, 2017. Google Scholar
  4. Olaf Beyersdorff and Joshua Blinkhorn. Lower bound techniques for QBF expansion. Theory of Computing Systems, 64(3):400-421, 2020. URL: https://doi.org/10.1007/s00224-019-09940-0.
  5. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. Logical Methods in Computer Science, Volume 15, Issue 1, February 2019. URL: https://doi.org/10.23638/LMCS-15(1:13)2019.
  6. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building Strategies into QBF Proofs. Journal of Automated Reasoning, 2020. Preliminary version in 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). URL: https://doi.org/10.1007/s10817-020-09560-1.
  7. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Hardness characterisations and size-width lower bounds for QBF resolution. In Proc. ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 209-223. ACM, 2020. Google Scholar
  8. Olaf Beyersdorff, Ilario Bonacina, and Leroy Chew. Lower bounds: From circuits to QBF proof systems. In ACM Conference on Innovations in Theoretical Computer Science (ITCS), pages 249-260, 2016. Google Scholar
  9. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified Boolean logic. J. ACM, 67(2), 2020. Google Scholar
  10. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. New Resolution-Based QBF Calculi and Their Proof Complexity. ACM Trans. Comput. Theory, 11(4), September 2019. URL: https://doi.org/10.1145/3352155.
  11. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Feasible interpolation for QBF resolution calculi. Logical Methods in Computer Science, 13, 2017. Google Scholar
  12. Olaf Beyersdorff, Leroy Chew, Meena Mahajan, and Anil Shukla. Understanding cutting planes for QBFs. Information and Computation, 262:141-161, 2018. Google Scholar
  13. Olaf Beyersdorff, Leroy Chew, and Karteek Sreenivasaiah. A game characterisation of tree-like Q-Resolution size. J. Comput. Syst. Sci., 104:82-101, 2019. Google Scholar
  14. Olaf Beyersdorff, Luke Hinde, and Ján Pich. Reasons for hardness in QBF proof systems. ACM Transactions on Computation Theory, 12(2), 2020. Google Scholar
  15. Nikolaj Bjørner, Mikolás Janota, and William Klieber. On conflicts and strategies in QBF. In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning LPAR 2015, volume 35 of EPiC Series in Computing, pages 28-41. EasyChair, 2015. Google Scholar
  16. A. Blake. Canonical expressions in boolean algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  17. Beate Bollig and Ingo Wegener. A very simple function that requires exponential size read-once branching programs. Information Processing Letters, 66(2):53-57, 1998. URL: https://doi.org/10.1016/S0020-0190(98)00042-8.
  18. Samuel R. Buss. Towards NP-P via proof complexity and search. Ann. Pure Appl. Logic, 163(7):906-917, 2012. Google Scholar
  19. 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
  20. 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-19, pages 291-308, 2013. Google Scholar
  21. Marijn Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In IJCAR, pages 91-106, 2014. Google Scholar
  22. Mikoláš Janota. On Q-Resolution and CDCL QBF solving. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, pages 402-418, Cham, 2016. Springer International Publishing. Google Scholar
  23. Mikoláš Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theoretical Computer Science, 577:25-42, 2015. URL: https://doi.org/10.1016/j.tcs.2015.01.048.
  24. Manuel Kauers and Martina Seidl. Short proofs for some symmetric quantified Boolean formulas. Inf. Process. Lett., 140:4-7, 2018. Google Scholar
  25. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  26. Jan Krajíček. Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, Cambridge, 1995. Google Scholar
  27. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-resolution with generalized axioms. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 435-452. Springer, 2016. Google Scholar
  28. Jakob Nordström. On the interplay between proof complexity and SAT solving. SIGLOG News, 2(3):19-44, 2015. Google Scholar
  29. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Long-distance Q-resolution with dependency schemes. J. Autom. Reasoning, 63(1):127-155, 2019. Google Scholar
  30. Tomás Peitl, Friedrich Slivovsky, and Stefan Szeider. Proof complexity of fragments of long-distance Q-resolution. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 319-335. Springer, 2019. Google Scholar
  31. Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17). Artif. Intell., 274:224-248, 2019. Google Scholar
  32. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12:23-41, 1965. Google Scholar
  33. Ankit Shukla, Armin Biere, Luca Pulina, and Martina Seidl. A survey on applications of quantified Boolean formulas. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, pages 78-84, 2019. Google Scholar
  34. Friedrich Slivovsky and Stefan Szeider. Soundness of Q-resolution with dependency schemes. Theoretical Computer Science, 612:83-101, 2016. Google Scholar
  35. G. S. Tseitin. On the complexity of derivation in propositional calculus. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, pages 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
  36. 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
  37. Ingo Wegener. Branching Programs and Binary Decision Diagrams. Society for Industrial and Applied Mathematics, 2000. URL: https://doi.org/10.1137/1.9780898719789.
  38. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In IEEE/ACM International Conference on Computer-aided Design, ICCAD 2002, 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