Document Open Access Logo

Relating Existing Powerful Proof Systems for QBF

Authors Leroy Chew , Marijn J. H. Heule

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2022.10.pdf
  • Filesize: 0.81 MB
  • 22 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • QBF
  • Proof Complexity
  • Verification
  • Strategy Extraction
  • Sequent Calculus

Metrics

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

Abstract

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not have strategy extraction. Because EUR heavily uses resolution paths our technique also brings resolution path dependency and sequent systems closer together. While we do not recommend G for practical applications this work can potentially show what features are needed for a new QBF checking format stronger than QRAT.

Cite As Get BibTex

Leroy Chew and Marijn J. H. Heule. Relating Existing Powerful Proof Systems for QBF. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.SAT.2022.10

Author Details

Leroy Chew
  • TU Wien, Austria
Marijn J. H. Heule
  • Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Chew, Leroy: Supported by the Vienna Science and Technology Fund (WWTF) under grant ICT19-060.
  • Heule, Marijn J. H.: Supported by National Science Foundation grant CCF-2015445.

References

  1. Olaf Beyersdorff, Ilario Bonacina, Leroy Chew, and Jan Pich. Frege systems for quantified boolean logic. J. ACM, 67(2), April 2020. URL: https://doi.org/10.1145/3381881.
  2. Leroy Chew and Judith Clymo. The equivalences of refutational QRAT. In Mikolás Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, volume 11628 of Lecture Notes in Computer Science, pages 100-116. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_7.
  3. Leroy Chew and Judith Clymo. How QBF expansion makes strategy extraction hard. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 66-82. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51074-9_5.
  4. Leroy Chew and Friedrich Slivovsky. Towards uniform certification in QBF. Electron. Colloquium Comput. Complex., page 144, 2021. URL: https://eccc.weizmann.ac.il/report/2021/144.
  5. Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:68-131, 1935. Google Scholar
  6. Marijn J.H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. Journal of Automated Reasoning, 64(3):533-554, 2020. Google Scholar
  7. Marijn J.H. Heule, Martina Seidl, and Armin Biere. Efficient extraction of skolem functions from qrat proofs. 2014 Formal Methods in Computer-Aided Design, FMCAD 2014, pages 107-114, December 2014. URL: https://doi.org/10.1109/FMCAD.2014.6987602.
  8. Marijn J.H. Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In 7th International Joint Conference on Automated Reasoning (IJCAR), pages 91-106, 2014. Google Scholar
  9. Marijn J.H. Heule, Martina Seidl, and Armin Biere. A unified proof system for QBF preprocessing. In Automated Reasoning - 7th International Joint Conference, IJCAR, volume 8562, pages 91-106. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08587-6_7.
  10. Mikolás Janota. QFUN: towards machine learning in QBF. CoRR, abs/1710.02198, 2017. URL: http://arxiv.org/abs/1710.02198.
  11. Benjamin Kiesl, Marijn J. H. Heule, and Martina Seidl. A little blocked literal goes a long way. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017, pages 281-297, Cham, 2017. Springer International Publishing. Google Scholar
  12. Benjamin Kiesl and Martina Seidl. QRAT polynomially simulates ∀Exp+Res. In Mikoláš Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019, pages 193-202, Cham, 2019. Springer International Publishing. Google Scholar
  13. Hans Kleine Büning and Uwe Bubeck. Theory of quantified Boolean formulas. In Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 735-760. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-735.
  14. Hans Kleine Büning, Marek Karpinski, and Andreas Flögel. Resolution for quantified Boolean formulas. Inf. Comput., 117(1):12-18, 1995. URL: https://doi.org/10.1006/inco.1995.1025.
  15. Jan Krajíček. Proof complexity. In European congress of mathematics (ECM), pages 221-231. Stockholm, Sweden, Zurich: European Mathematical Society, 2005. Google Scholar
  16. Jan Krajíček and Pavel Pudlák. Quantified propositional calculi and fragments of bounded arithmetic. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 36:29-46, 1990. Google Scholar
  17. Leander Tentrup. CAQE and quabs: Abstraction based QBF solvers. J. Satisf. Boolean Model. Comput., 11(1):155-210, 2019. URL: https://doi.org/10.3233/SAT190121.
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