2026-09-18T02:43:11Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23759 2026-09-05T18:29:42Z ddc:004 open_access

QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms Peyrer, Mark Seidl, Martina Automated Reasoning Quantified Resolution Proof Generalized Axioms 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mark Peyrer and Martina Seidl 2025 Is Part Of LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2025.25 urn:nbn:de:0030-drops-237592 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.25 eng https://creativecommons.org/licenses/by/4.0/legalcode