Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking

Technical Summary: Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking

Problem Statement
Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) remains a significant challenge. While recent proof complexity research has demonstrated that the "Independent Extension" rule (IndExt) allows the proof system IndExtQURes to p-simulate the vast majority of existing QBF and DQBF techniques, IndExtQURes itself is not yet a practical certification format. Conversely, practical formats like QRAT (Quantified Resolution Asymmetric Tautology) and its DQBF generalization DQRAT (Dependency Quantified Resolution Asymmetric Tautology) lack the theoretical strength to p-simulate IndExtQURes. Specifically, DQRAT, which relies on the reflexive resolution path dependency scheme ($D_{rrs}$), has not been proven to match the power of IndExtQURes, leaving a gap between theoretical optimality and practical certification.

Methodology
The authors address this gap by introducing a new dependency scheme called $D_{\forall pure}$ (Pure Universal Dependency Scheme). This scheme is based on the concept of "pure paths," which restricts resolution paths between universal and existential literals. Unlike the standard reflexive resolution path ($D_{rrs}$), $D_{\forall pure}$ excludes resolution paths from a universal literal $u$ to an existential literal $x$ if the path is merely an extension of a path from $\bar{u}$ to $x$. This ensures that only minimal, necessary dependencies are retained.

The methodology involves three main components:

1. Definition and Soundness: The authors formally define $D_{\forall pure}$ using fixpoint constructions on sets of clauses and literals. They prove the semantic soundness of this scheme (Theorem 10), demonstrating that removing spurious dependencies identified by $D_{\forall pure}$ preserves the truth value of the DQBF.
2. Integration into Proof Systems: The authors integrate $D_{\forall pure}$ into the DQRAT proof system, creating a new system denoted as DQRAT+$D_{\forall pure}$. They also define a local reduction rule, Loc$_{\forall pure}$-Red, which allows for the direct reduction of clauses containing universal literals without altering the prefix, provided no pure paths exist to conflicting clauses.
3. Complexity Analysis: The paper establishes the relationship between the new system and IndExtQURes. The authors prove that DQRAT+$D_{\forall pure}$ and IndExtQURes are p-equivalent (polynomial-time equivalent). This is achieved by showing that DQRAT+$D_{\forall pure}$ can p-simulate IndExtQURes (by simulating the Independent Extension rule using the new dependency scheme to remove unnecessary dependencies) and that IndExtQURes can p-simulate DQRAT+$D_{\forall pure}$.

Key Contributions

• New Dependency Scheme ($D_{\forall pure}$): The paper introduces a dependency scheme that is strictly stronger than $D_{rrs}$ in specific contexts (e.g., separating LD-Q(Drrs)-Res from LD-Q(D$_{\forall pure}$)-Res) while maintaining polynomial-time checkability.
• Proof System Equivalence: The primary theoretical contribution is the proof that DQRAT+$D_{\forall pure}$ is p-equivalent to IndExtQURes. This implies that DQRAT+$D_{\forall pure}$ can p-simulate all major QBF and DQBF proof systems that IndExtQURes can, including QRAT, G, and various dependency scheme rules.
• Strategy Extraction: The authors show that $D_{\forall pure}$ is a "normal" dependency scheme, which allows for polynomial-time strategy extraction in Long-Distance Q-Resolution (LD-Q-Res). This result supports the sound integration of $D_{\forall pure}$ into solvers like Qute.
• Implementation: The authors implemented a prototype proof checker, DQRAT-check, which supports the DQRAT+$D_{\forall pure}$ format. They also extended the Qute solver to utilize $D_{\forall pure}$ for clause learning.

Results

• Theoretical: The paper demonstrates that $D_{\forall pure}$ allows for the removal of dependencies that $D_{rrs}$ cannot, specifically in cases involving "bridged" parity formulas where $D_{rrs}$ fails to detect independence but $D_{\forall pure}$ succeeds.
• Experimental (Proof Checking): The prototype checker was tested on benchmarks from QBFEval 2022 and crafted formulas (including the examples from the paper). The checker successfully verified proofs. The authors note that proof extraction and conversion from QRP (Qute's internal format) to DQRAT accounts for 97% of the checking time, while the DQRAT-checker itself accounts for only 3%.
• Experimental (Solving): When integrated into the Qute solver, $D_{\forall pure}$ showed promise on QBFEval 2020 benchmarks, reducing dependency computation time by 7x and finding twice as many independent pairs compared to $D_{rrs}$. However, on the newer QBFEval 2022 benchmarks, $D_{\forall pure}$ detected no new independencies, and the overhead did not improve the number of solved instances or PAR2 scores.

Significance
The paper claims that its primary significance lies in bridging the gap between theoretical proof strength and practical certification formats. By showing that a simple modification to the existing DQRAT framework (adding the $D_{\forall pure}$ rule) yields a system p-equivalent to the powerful IndExtQURes, the authors provide a path toward a unified, strong certification standard for both QBF and DQBF. This avoids the need to prove p-simulations for every individual proof system against IndExtQURes, relying instead on the transitivity of the equivalence between DQRAT+$D_{\forall pure}$ and IndExtQURes. Furthermore, the work provides a concrete implementation (DQRAT-check) and demonstrates the feasibility of integrating these strong dependency schemes into existing solving infrastructure, paving the way for more robust certification in future DQBF solvers.