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

The solving landscape for quantified Boolean formulas (QBFs) is very heterogeneous [17]. In contrast to SAT, which has conflict-driven clause learning (CDCL) [18] as predominant solving paradigm, the situation is less clear for QBFs. Besides QCDCL, the CDCL variant for QBF, expansion- and abstraction-based approaches have proven to be very powerful and of orthogonal strength [11]. To combine different approaches, different directions are taken: a very loose integration is obtained by portfolio-based solving [9, 8] and by pre- and inprocessing [5, 14]. A very tight integration is based on the idea of learning generalized axioms [15]: during search QCDCL solvers learn clauses (conflicts) and cubes (solutions) that are justified by Q-resolution [10]. A generalized axiom is a clause or cube that is learned by calling an oracle solver. Such an oracle can be any complete or incomplete QBF solver.

So far, the usage of generalized axioms has one major drawback: if used in a Q-resolution proof, the QBF variant of resolution proofs as produced by QCDCL solvers, its correctness has no justification, because it was derived by using an oracle solver. Consequently, Q-resolution proofs that rely on generalized axioms cannot be checked by an independent checking tool and the result of the QBF solver cannot be certified. Therefore, generalized axioms have to be disabled if a certificate is required.

To overcome this limitation and certify the correctness of Q-resolution proofs with generalized axioms, we present the novel certification framework QRP+Gen which extends the Q-resolution certification framework QRPcheck with generalized axioms. To this end, we furthermore extended the Q-resolution format QRP to incorporate their certification. As a proof-of-concept we equipped the QCDCL-based solver DepQBF [13] with proof generation for generalized axioms obtained by deciding certain propositional abstractions of the considered QBF. Our implementation is publicly available at

https://doi.org/10.5281/zenodo.16307432

Traditional search-based QBF solving with conflict-driven clause learning and solution-driven cube learning (QCDCL) [23, 7] successively generates variable assignments for a given QBF $\varphi =\mathrm{\Pi }:\mathrm{\Psi }$ until $\varphi$ is decided. Usually $\varphi$ is in prenex conjunctive normal form (PCNF). Here, $\mathrm{\Pi }=Q_1{x}_1,\mathrm{\dots }{Q}_n{x}_n$ is a quantifier prefix with $Q_i\in \{\forall ,\exists \}$ and the propositional matrix $\mathrm{\Psi }$ is a conjunction of clauses. A clause is a disjunction of literals and a literal is a variable or a negated variable. Note that not every variable that occurs in the matrix has to be part of the prefix (free variables). In contrast to SAT, variables may not be assigned in an arbitrary order, but the dependencies imposed by the quantifier prefix have to be considered. Still, clauses are learned from assignments that falsify the formula to prune the search space. In addition, also cubes (conjunctions of literals) are learned from assignments that satisfy the propositional part of the formula (solutions). While clauses are conjunctively added to the propositional matrix, cubes are disjunctively collected in a cube database. The addition of clauses and cubes preserves the truth/falsity of the original formula, because they are derived via some variant of Q-resolution, the extension of propositional resolution for QBF. On this basis, QCDCL solvers can produce Q-resolution proofs as certificates for the solving results. For false QBFs, clause Q-resolution proofs are generated, and, dually, cube Q-resolution proofs are generated for true formulas. Both types of proofs can efficiently be checked [20]. We want to underline how Q-resolution is in general not expressive enough for QCDCL, which causes the need to disable certain techniques in actual implementations when proof generation is required.

In general, learning smaller clauses and cubes w.r.t the amount of literals is favorable during the search. However, in classical QCDCL implementations, especially large cubes are learned because the cube database is empty in the beginning. Hence, there are no cubes serving as axioms in cube Q-resolution proofs. To initialize the cube database, assignments satisfying the propositional matrix are taken, from which smaller cubes are derived until the empty cube is found [24]. Axioms of clausal Q-resolution proofs are the clauses from the propositional matrix of the original formula.

To learn smaller clauses and cubes faster, the concept of generalized axioms has been introduced [15]. Consider a QBF $\varphi =\mathrm{\Pi }:\mathrm{\Psi }$ and assume that during the search a partial assignment $\sigma =\{l_1,\mathrm{\dots },l_n\}$ has been found respecting the dependencies imposed by the quantifier prefix. If a variable $x\in \sigma$, then $x$ is set to true, whereas if $\neg x\in \sigma$, then $x$ is set to false. Furthermore, there is no variable $x$ with $x,\neg x\in \sigma$. Now assume that ${\varphi }^{\prime }=\varphi [\sigma ]$ is not decided where $\varphi [\sigma ]$ is the formula obtained by assigning all variables according to $\sigma$. Using an oracle solver that is able to decide ${\varphi }^{\prime }$, either a clause or a cube can be learned dependent on the value of ${\varphi }^{\prime }$. If ${\varphi }^{\prime }$ is false, then the clause $({\overline{l}}_1\vee \mathrm{\dots }\vee {\overline{l}}_n)$ can be learned. Otherwise, the cube $(l_1\wedge \mathrm{\dots }\wedge l_n)$ can be learned. The oracle can be any solver that is able to decide a QBF. It could be, for example, a solver that is based on a decision procedure of orthogonal strength like expansion-based solving [11]. Also incomplete methods can be used as oracles. If no solution is found, then the QCDCL search is resumed under the assignment $\sigma$. The following example illustrates the power of the approach.

The only problem with this approach is that the proof containing generalized axioms is not a valid certificate for the solving result, because the axioms are not justified. For this reason, QCDCL solvers do not provide certificates when generalized axioms are enabled so far. Therefore, no independent checking is possible and the result of the solver (and the internally called oracles) has to be trusted without witness.

To enable certification for QCDCL solvers that use solver oracles to learn generalized axioms either in terms of clauses or cubes, we developed the QRP+Gen framework. It is based on the QRPcheck certification tool chain [19] which provides a checker for Q-resolution proofs in the QRP format. To close the holes in the proofs introduced by generalized axioms, the oracles have to also provide witnesses which are used to justify the soundness of the learned axioms. The general architecture of our framework is shown in Figure 1 which allows for an automatic integration of the different proofs giving a full witness for the input formula.

In the following, we present how we extended the QBF solver DepQBF to obtain certificates for generalized axioms that use two SAT solvers as oracles. The SAT solvers are called with certain propositional abstractions of the input QBF under the current assignment $\sigma$. Clauses and cubes learned as generalized axioms are justified by the techniques Trivial Truth and Trivial Falsity [6, 15]. To certify the correctness of such generalized axioms, different types of proofs are combined as shown in Figure 3. In addition, DepQBF learns generalized axioms by calling the expansion-based solver Nenofex [12] which is not able to produce proofs. Extending Nenofex with proof generation capabilities is beyond the scope of this work, hence we disabled learning generalized axioms with Nenofex. In the original implementation, DepQBF employed PicoSAT [3] as SAT solver. Instead of PicoSAT, we use the latest version of the SAT solver CaDiCaL [4] which is able to produce DRAT proofs [22].¹¹1We thank Maximilian Heisinger for integrating CaDiCaL into DepQBF.

We conducted two experiments showing the impact of QRP+Gen applied on the previously described case study. Both experiments were executed on a Ubuntu 24.04 machine with dual-socket AMD EPYC 7313@$3.7\mathrm{GHz}$ CPUs. We assigned $8\mathrm{GB}$ RAM as well as $1\mathrm{h}$ per task as resource limitations.

We presented QRP+Gen, the – to the best of our knowledge – first framework allowing certificates for reasoning with generalized axioms. We extended the well-established QRP proof format with justifications for clauses and cubes derived by generalized axioms based on results obtained from oracle solvers. In our framework, any oracle solver able to produce proofs for which checking tools are available can be considered.

As a case study, we implemented proof generation and checking for generalized axioms obtained by the abstraction-based techniques trivial truth and trivial falsity in the solver DepQBF. We evaluated the framework on different types of benchmarks and observed only little overhead caused by proof generation. With our framework, it is now possible to independently confirm the result of a QBF solver that relies on general axioms.

The presented approach is, however, not limited to generalized axioms. Our framework can be employed in other scenarios where different solving systems based on different proof systems are combined. Potential applications include interfacing proofs produced by preprocessing tools and complete solvers. Our framework could also be applied in the context of cube&conquer-based solving [8].