Document Open Access Logo

Classes of Hard Formulas for QBF Resolution

Authors Agnes Schleitzer, Olaf Beyersdorff

PDF
Thumbnail PDF

File

LIPIcs.SAT.2022.5.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Agnes Schleitzer
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany
Olaf Beyersdorff
  • Institut für Informatik, Friedrich-Schiller-Universität Jena, Germany

Funding

  • Schleitzer, Agnes: DFG grant BE 4209/3-1.
  • Beyersdorff, Olaf: Carl-Zeiss Foundation and DFG grant BE 4209/3-1.

Cite AsGet BibTex

Agnes Schleitzer and Olaf Beyersdorff. Classes of Hard Formulas for QBF Resolution. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.SAT.2022.5

Abstract

To date, we know only a few handcrafted quantified Boolean formulas (QBFs) that are hard for central QBF resolution systems such as Q-Res and QU-Res, and only one specific QBF family to separate Q-Res and QU-Res. Here we provide a general method to construct hard formulas for Q-Res and QU-Res. The construction uses simple propositional formulas (e.g. minimally unsatisfiable formulas) in combination with easy QBF gadgets (Σ₂^b formulas without constant winning strategies). This leads to a host of new hard formulas, including new classes of hard random QBFs. We further present generic constructions for formulas separating Q-Res and QU-Res, and for separating Q-Res and LD-Q-Res.

Subject Classification

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

Metrics

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

References

  1. Hoda Abbasizanjani. The combinatorics of minimal unsatisfiability: connecting to graph theory. dissertation, Department of Computer Science, Swansea University, 2021. Google Scholar
  2. Hoda Abbasizanjani and Oliver Kullmann. Minimal unsatisfiability and minimal strongly connected digraphs. In Olaf Beyersdorff and Christoph M. Wintersteiger, editors, Theory and Applications of Satisfiability Testing (SAT), volume 10929 of Lecture Notes in Computer Science, pages 329-345. Springer, 2018. Google Scholar
  3. Hoda Abbasizanjani and Oliver Kullmann. Classification of minimally unsatisfiable 2-cnfs. CoRR, abs/2003.03639, 2020. URL: http://arxiv.org/abs/2003.03639.
  4. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res., 40:353-373, 2011. Google Scholar
  5. Valeriy Balabanov and Jie-Hong R. Jiang. Unified QBF certification and its applications. Formal Methods in System Design, 41(1):45-65, 2012. URL: https://doi.org/10.1007/s10703-012-0152-6.
  6. 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), pages 154-169, 2014. Google Scholar
  7. P. Beame and T. Pitassi. Simplified and improved resolution lower bounds. In Proc. 37th IEEE Symposium on the Foundations of Computer Science, pages 274-281. IEEE Computer Society Press, 1996. Google Scholar
  8. Paul Beame, Henry A. Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. (JAIR), 22:319-351, 2004. URL: https://doi.org/10.1613/jair.1410.
  9. Olaf Beyersdorff and Joshua Blinkhorn. Lower bound techniques for QBF expansion. Theory Comput. Syst., 64(3):400-421, 2020. Google Scholar
  10. Olaf Beyersdorff and Joshua Blinkhorn. A simple proof of QBF hardness. Information Processing Letters, 168, 2021. Google Scholar
  11. Olaf Beyersdorff, Joshua Blinkhorn, and Luke Hinde. Size, cost, and capacity: A semantic technique for hard random QBFs. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  12. 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
  13. Olaf Beyersdorff, Joshua Blinkhorn, and Meena Mahajan. Building strategies into QBF proofs. J. Autom. Reasoning, 65(1):125-154, 2021. Google Scholar
  14. Olaf Beyersdorff and Benjamin Böhm. Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. In 12th Innovations in Theoretical Computer Science Conference (ITCS 2021), volume 185 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:20, 2021. Google Scholar
  15. Olaf Beyersdorff, Leroy Chew, and Mikolás Janota. New resolution-based QBF calculi and their proof complexity. ACM Transactions on Computation Theory, 11(4):26:1-26:42, 2019. Google Scholar
  16. Olaf Beyersdorff and Luke Hinde. Characterising tree-like Frege proofs for QBF. Inf. Comput., 268, 2019. Google Scholar
  17. 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
  18. Olaf Beyersdorff, Mikolás Janota, Florian Lonsing, and Martina Seidl. Quantified boolean formulas. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 1177-1221. IOS Press, 2021. Google Scholar
  19. Olaf Beyersdorff, Luca Pulina, Martina Seidl, and Ankit Shukla. Qbffam: A tool for generating QBF families from proof complexity. In Chu-Min Li and Felip Manyà, editors, Theory and Applications of Satisfiability Testing (SAT), volume 12831 of Lecture Notes in Computer Science, pages 21-29. Springer, 2021. Google Scholar
  20. 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
  21. 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. URL: https://doi.org/10.1137/S0097539799352474.
  22. Sam Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, pages 233-350. IOS Press, 2021. Google Scholar
  23. Leroy Chew. QBF proof complexity. PhD thesis, University of Leeds, Leeds, 2017. Google Scholar
  24. Leroy Chew and Friedrich Slivovsky. Towards uniform certification in QBF. Electron. Colloquium Comput. Complex., 2021. To appear at STACS 2022. URL: https://eccc.weizmann.ac.il/report/2021/144.
  25. Judith Clymo. Proof Complexity for Quantified Boolean Formulas. PhD thesis, School of Computing, University of Leeds, 2021. Google Scholar
  26. Stephen A. Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, 2010. Google Scholar
  27. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  28. Uwe Egly, Florian Lonsing, and Magdalena Widl. Long-distance resolution: Proof generation and strategy extraction in search-based QBF solving. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pages 291-308, 2013. Google Scholar
  29. Amin Haken. The intractability of resolution. Theoretical Computer Science, 39:297-308, 1985. Google Scholar
  30. Mikolás Janota and Joao Marques-Silva. Expansion-based QBF solving versus Q-resolution. Theor. Comput. Sci., 577:25-42, 2015. Google Scholar
  31. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. Google Scholar
  32. 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
  33. Jan Krajíček. Proof complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, 2019. Google Scholar
  34. Florian Lonsing, Uwe Egly, and Allen Van Gelder. Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In Proc. International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 100-115, 2013. Google Scholar
  35. 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
  36. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. URL: https://doi.org/10.1016/j.artint.2010.10.002.
  37. Nathan Segerlind. The complexity of propositional proofs. Bulletin of Symbolic Logic, 13(4):417-481, 2007. Google Scholar
  38. M. Sipser. Introduction to the Theory of Computation. Course Technology, 2nd edition, February 2005. Google Scholar
  39. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. Google Scholar
  40. Allen Van Gelder. Contributions to the theory of practical quantified Boolean formula solving. In Proc. Principles and Practice of Constraint Programming (CP), pages 647-663, 2012. Google Scholar
  41. 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), 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