Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking
Source: arXiv:2605.29763 · Published 2026-05-28 · By Leroy Chew, Tomáš Peitl
TL;DR
This paper addresses a critical challenge in certification and proof checking for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF). Prior work showed that many QBF and DQBF proof techniques could be polynomially simulated by the Independent Extension (IndExt) rule, a powerful but theoretically defined proof rule that had no practical proof checker counterpart. The authors introduce a new dependency scheme called the pure universal dependency scheme (D∀pure), which when added to the existing DQRAT proof system, yields a system (DQRAT + D∀pure) that is p-equivalent to IndExtQURes, the strongest known DQBF/QBF proof system. They implement a prototype proof checker, DQRAT-check, to validate this addition. The D∀pure scheme also possesses desirable theoretical properties allowing sound integration in solver frameworks such as Qute for dependency learning. By bridging the gap between theory and practice, this work advances scalable, polynomial-time checking of sophisticated DQBF proofs that incorporate advanced dependency reasoning previously only available in theory.
Their results provide both theoretical p-equivalence proofs between DQRAT+D∀pure and IndExtQURes, and demonstrate practical feasibility through the prototype proof checker implementation. They also prove that D∀pure can be applied as an effective prefix modification rule, enabling efficient recalculation of dependency sets in polynomial time without losing correctness. Example QBFs and formal proof derivations illustrate this approach and distinguish D∀pure from prior dependency schemes such as Drrs.
Key findings
- Adding the pure universal dependency scheme (D∀pure) to DQRAT makes it p-equivalent to IndExtQURes, the strongest known QBF/DQBF proof system.
- D∀pure allows polynomial-time recalculation of dependency sets in a DQBF prefix, soundly removing spurious dependencies.
- Prototype implementation DQRAT-check supports the new D∀pure rule, showing practical feasibility of this theoretical advance.
- D∀pure strictly strengthens the reflexive resolution path dependency scheme (Drrs) by excluding resolution paths extended from the negated universal literal.
- The integration of D∀pure enables strategy extraction within resolution proof systems, supporting sound use in dependency learning solvers like Qute.
- Example 8 distinguishes D∀pure from Drrs by showing fewer dependencies, demonstrating improved precision in dependency analysis.
- The paper provides a soundness proof (Theorem 10) that modifying a true DQBF’s prefix according to D∀pure preserves truth.
- The D∀pure sets L∀pure and C∀pure can be computed in linear time w.r.t. the formula size (number of literals).
Threat model
The adversary is a proof generator that may provide unsound or invalid proofs of QBF/DQBF formulas to the verifier. The verifier must efficiently and soundly check proof validity, confirming that added or removed dependency relations do not invalidate the formula’s truth. The adversary cannot forge proofs that fool the verifier under the D∀pure rule or break its soundness guarantees, as the proof checker relies on formal dependency schemes and polynomial-time checks with strict conditions. The adversary is limited to manipulating proof representations and dependencies, but cannot feasibly circumvent the soundness of the D∀pure-enhanced DQRAT checking framework.
Methodology — deep read
The paper focuses on certification and proof systems for QBFs and DQBFs, where the key element is managing variable dependencies that affect proof strength and solver efficiency. The threat model involves a verifier checking correctness of QBF/DQBF proofs generated by solvers or preprocessing. The adversary might produce invalid proofs, so the system must efficiently and soundly confirm proof validity under relaxed dependency conditions.
The authors build on the DQRAT proof system, which generalizes RAT rules to DQBF and supports dependency reasoning based on known schemes like reflexive resolution path dependencies (Drrs). They identify a missing ingredient: a stronger dependency scheme (D∀pure) based on "pure paths" which refine the dependency relation by excluding resolution paths that extend from the negation of universal literals.
They define D∀pure sets C∀pure and L∀pure via fixpoint expansions over clauses containing a given universal literal u, excluding clauses containing ¯u, to identify which existential literals depend on u. This dependency scheme is formally defined with clear logical conditions involving paths between literals.
They prove soundness by constructing suitable Skolem functions avoiding the spurious dependencies removed by D∀pure, showing truth preservation when modifying the DQBF prefix according to this scheme (Theorem 10).
A prototype proof checker, DQRAT-check, is implemented that extends the existing DQRAT checker to handle D∀pure’s refined dependency set computations efficiently. They demonstrate example proofs for canonical formulas previously not manageable by simpler schemes, validating correctness and illustrating the practical utility of their rule.
They also discuss the theoretical complexity of computing D∀pure, showing it can be done in linear time in the number of literals, enabling efficient prefix modification in polynomial time.
The evaluation involves detailed logical and proof complexity analyses rather than extensive empirical benchmarking. They relate their systems through p-simulation arguments and illustrate key examples to distinguish their new scheme from prior dependency schemes like Drrs.
This rigorous approach bridges the gap from theoretical proof complexity to practical, checkable DQBF proof systems able to capture state-of-the-art reasoning techniques with soundness and scalability guarantees.
Technical innovations
- Introduction of the pure universal dependency scheme (D∀pure) that refines dependency detection by excluding resolution paths extended from negated universal literals.
- Proof that adding D∀pure to DQRAT yields a system p-equivalent to Independent Extended QU-Res, a highly powerful QBF/DQBF proof system.
- Definition of polynomial-time computable sets C∀pure and L∀pure for dependency checking, enabling efficient prefix modifications at scale.
- Implementation of a prototype proof checker DQRAT-check extended with D∀pure that supports practical certification of enhanced DQBF proofs.
Baselines vs proposed
- DQRAT (without D∀pure): p-simulated by IndExtQURes (previously open whether converse p-simulation possible)
- DQRAT + D∀pure: shown p-equivalent to IndExtQURes, thus strictly stronger than baseline DQRAT
- Reflexive resolution path dependency scheme (Drrs): D∀pure outperforms by excluding spurious dependencies in key examples (e.g. Example 8).
Limitations
- Experimental evaluation is limited to proof-of-concept examples and theoretical arguments; large-scale benchmarking on QBF/DQBF solver benchmarks is not provided.
- The prototype proof checker DQRAT-check is described but detailed performance metrics or comparisons are omitted.
- Some complexity analysis assumes idealized implementations; practical engineering and integration with existing solvers such as Qute may require further work.
- The p-equivalence proofs rely on non-trivial proof complexity theory rather than constructive transformations explicitly detailed for all cases.
- D∀pure’s polynomial-time checkability holds theoretically, but worst-case complexity may still be significant for very large or complex formulas.
Open questions / follow-ons
- How does D∀pure scaling behave in large real-world QBF/DQBF benchmarks compared to other dependency schemes?
- Can the D∀pure dependency scheme be integrated seamlessly into state-of-the-art DQBF solvers for preprocessing or in-processing dependency learning?
- Are there stronger or orthogonal dependency schemes beyond D∀pure that can extend certification power further while remaining polynomial-time checkable?
- What are the trade-offs between proof size and verification time when using D∀pure versus other dependency schemes in practical proof logging?
Why it matters for bot defense
Bot-defense and CAPTCHA practitioners typically rely on robust cryptographic or heuristic methods rather than formal QBF or DQBF proofs. However, this paper’s insights into dependency schemes and polynomial-time certification mechanisms can be valuable when designing proof-carrying authentication or challenge-response protocols where correctness and efficient verifiability are essential.
Specifically, the refinement of dependency detection via D∀pure and the practical prototype checker demonstrate ways to improve reliability and scalability of proof verification under complex logical dependencies. This approach may inspire designs for bot-proof protocols involving quantified assertions or for formal verification of automated reasoning components within a CAPTCHA system. The principle of sound but efficient dependency relaxations could, in theory, be applied to improve solver-based anti-bot algorithms that use logical reasoning or constraint certification.
Cite
@article{arxiv2605_29763,
title={ Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking },
author={ Leroy Chew and Tomáš Peitl },
journal={arXiv preprint arXiv:2605.29763},
year={ 2026 },
url={https://arxiv.org/abs/2605.29763}
}