Document Open Access Logo

QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms

Authors Mark Peyrer , Martina Seidl

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.25.pdf
  • Filesize: 0.87 MB
  • 10 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.25.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Automated Reasoning
  • Quantified Resolution Proof
  • Generalized Axioms

Metrics

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

Abstract

Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers. 
While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.

Cite As Get BibTex

Mark Peyrer and Martina Seidl. QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 25:1-25:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.25

Author Details

Mark Peyrer
  • Institute for Symbolic Artificial Intelligence, Johannes Kepler University, Linz, Austria
Martina Seidl
  • Institute for Symbolic Artificial Intelligence, Johannes Kepler University, Linz, Austria

Funding

Parts of this work have been supported by the LIT AI Lab funded by the state of Upper Austria and by the Austrian Science Fund (FWF) [10.55776/COE12].

Supplementary Materials

References

  1. Olaf Beyersdorff, Leroy Chew, and Mikoláš Janota. New resolution-based QBF calculi and their proof complexity. ACM Transactions on Computation Theory, 11(4):1-42, 2019. URL: https://doi.org/10.1145/3352155.
  2. Olaf Beyersdorff, Luca Pulina, Martina Seidl, and Ankit Shukla. Qbffam: A tool for generating QBF families from proof complexity. In International Conference on Theory and Applications of Satisfiability Testing, pages 21-29. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-80223-3_3.
  3. Armin Biere. PicoSAT essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2-4):75-97, 2008. URL: https://doi.org/10.3233/SAT190039.
  4. Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. CaDiCaL 2.0. In 36th International Conference on Computer Aided Verification, pages 133-152. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65627-9_7.
  5. Armin Biere, Florian Lonsing, and Martina Seidl. Blocked clause elimination for QBF. In 23rd International Conference on Automated Deduction, pages 101-115. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_10.
  6. Marco Cadoli, Andrea Giovanardi, and Marco Schaerf. An algorithm to evaluate quantified boolean formulae. AAAI/IAAI, 98:262-267, 1998. URL: http://www.aaai.org/Library/AAAI/1998/aaai98-036.php.
  7. Enrico Giunchiglia, Massimo Narizzano, and Armando Tacchella. Clause/term resolution and learning in the evaluation of quantified boolean formulas. Journal of Artificial Intelligence Research, 26:371-416, 2006. URL: https://doi.org/10.1613/JAIR.1959.
  8. Maximilian Heisinger, Martina Seidl, and Armin Biere. Paraqooba: A fast and flexible framework for parallel and distributed QBF solving. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 426-447. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_22.
  9. Holger H Hoos, Tomáš Peitl, Friedrich Slivovsky, and Stefan Szeider. Portfolio-based algorithm selection for circuit qbfs. In 24th International Conference of Principles and Practice of Constraint Programming, pages 195-209. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_13.
  10. Mikoláš Janota. On Q-Resolution and CDCL QBF solving. In 19th International Conference on Theory and Applications of Satisfiability Testing, pages 402-418. Springer, 2016. Google Scholar
  11. 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.
  12. Florian Lonsing and Armin Biere. Nenofex: Expanding nnf for qbf solving. In 11th International Conference on Theory and Applications of Satisfiability Testing, pages 196-210. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-79719-7_19.
  13. Florian Lonsing and Uwe Egly. DepQBF 6.0: A search-based QBF solver beyond traditional QCDCL. In 26th International Conference on Automated Deduction, pages 371-384. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_23.
  14. Florian Lonsing and Uwe Egly. QRATPre+: effective QBF preprocessing via strong redundancy properties. In 22nd International Conference on Theory and Applications of Satisfiability Testing, pages 203-210. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_14.
  15. Florian Lonsing, Uwe Egly, and Martina Seidl. Q-Resolution with Generalized Axioms. In 19th International Conference on Theory and Applications of Satisfiability Testing, pages 435-452. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-40970-2_27.
  16. Florian Lonsing, Uwe Egly, and Allen Van Gelder. Efficient clause learning for quantified Boolean formulas via QBF pseudo unit propagation. In 16th International Conference on Theory and Applications of Satisfiability Testing, pages 100-115. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_9.
  17. Paolo Marin, Massimo Narizzano, Luca Pulina, Armando Tacchella, and Enrico Giunchiglia. Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows. Fundamenta Informaticae, 149(1-2):133-158, 2016. URL: https://doi.org/10.3233/FI-2016-1445.
  18. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Handbook of satisfiability, pages 133-182. ios Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  19. Aina Niemetz. QRPcheck. URL: https://fmv.jku.at/qrpcheck/.
  20. Aina Niemetz, Mathias Preiner, Florian Lonsing, Martina Seidl, and Armin Biere. Resolution-based Certificate Extraction for QBF: (tool presentation). In 15th International Conference on Theory and Applications of Satisfiability Testing, pages 430-435. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31612-8_33.
  21. Luca Pulina, Martina Seidl, and Simone Heisinger. QBFGallery 2023. URL: https://qbf23.pages.sai.jku.at/gallery/.
  22. Nathan Wetzler, Marijn JH Heule, and Warren A Hunt Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In 17th International Conference on Theory and Applications of Satisfiability Testing, pages 422-429. Springer, 2014. Google Scholar
  23. Lintao Zhang and Sharad Malik. Conflict driven learning in a quantified Boolean satisfiability solver. In IEEE/ACM international conference on Computer-aided design, pages 442-449, 2002. URL: https://doi.org/10.1145/774572.774637.
  24. Lintao Zhang and Sharad Malik. Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In International Conference on Principles and Practice of Constraint Programming, pages 200-215. Springer, 2002. URL: https://doi.org/10.1007/3-540-46135-3_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact