pith. sign in

arxiv: 2605.29763 · v1 · pith:GFKT34HVnew · submitted 2026-05-28 · 💻 cs.LO

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

Leroy Chew , Tom\'a\v{s} Peitl This is my paper

Pith reviewed 2026-06-29 00:17 UTC · model grok-4.3

classification 💻 cs.LO
keywords dependency schemesQBFDQBFproof systemsDQRATDpureproof checkingQU-Res
0
0 comments X

The pith

The Dpure dependency scheme completes the DQRAT proof system to achieve p-equivalence with Independent Extended QU-Res.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Dpure, a new dependency scheme for quantified Boolean formulas and dependency quantified Boolean formulas based on pure paths. This scheme is presented as the addition needed to extend the DQRAT proof system so that it becomes p-equivalent to Independent Extended QU-Res, the strongest known system for these formulas. The authors implement a prototype checker DQRAT-check that incorporates the new rule, moving DQRAT from theory to a working tool. They also establish further properties of Dpure that support its use in both proof checking and solving contexts such as dependency learning.

Core claim

Dpure is the missing ingredient that when added to Blinkhorn's proof system DQRAT allows it to be provably p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so a prototype checker DQRAT-check is implemented that includes the extra rule. Dpure is also shown to possess additional properties previously identified for other dependency schemes.

What carries the argument

The Dpure dependency scheme, defined via pure paths, which is added to DQRAT to strengthen its dependency handling and reach p-equivalence with Independent Extended QU-Res.

If this is right

  • DQRAT augmented with Dpure p-simulates all proofs from Independent Extended QU-Res.
  • The implemented DQRAT-check can verify proofs in the strongest known QBF and DQBF systems.
  • Dpure supports sound integration into dependency learning solvers such as Qute.
  • The additional properties of Dpure identified in the paper apply to practical solving and checking tasks.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Pure-path techniques for defining dependency schemes may extend to other QBF proof formats beyond DQRAT.
  • A working checker for the strongest system could enable certification of proofs that current tools reject as too complex.

Load-bearing premise

The Dpure scheme is formulated correctly and integrates soundly into DQRAT without introducing unsoundness or altering the proof system semantics.

What would settle it

A concrete QBF or DQBF instance together with a proof accepted by DQRAT-check that derives a contradiction from a satisfiable formula, or a known proof from Independent Extended QU-Res that DQRAT with Dpure cannot simulate.

read the original abstract

Certification for Quantified Boolean Formulas (QBF) and Dependency Quantified Boolean Formulas (DQBF) is an ongoing challenge. Recent proof complexity work has shown that the majority of QBF and DQBF techniques can be p-simulated by using the independent extension rule. In propositional logic, extension rules are supported by proof checkers using a more general RAT (Resolution Asymmetric Tautology) rule. The next step in (D)QBF certification would be to update these modern RAT formats to match the strength of this independent extension rule. In this paper we first introduce a new dependency scheme called Dpure. This rule is the missing ingredient that when added to Blinkhorn's proof system DQRAT allows it to be provably p-equivalent to the Independent Extended QU-Res, the most powerful of the known QBF and DQBF proof systems. Up until now, DQRAT has only existed in theory, so we implement a prototype checker DQRAT-check which includes our extra rule. In addition to its inclusion in our proof checker we show Dpure has other properties that have been found for previous dependency schemes, and each of these observations has potential in solving/checking including the sound integration into the dependency learning solver Qute.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The manuscript introduces a new dependency scheme Dpure defined via pure paths in (D)QBF. It claims that adding this scheme to Blinkhorn's DQRAT proof system yields a system p-equivalent to Independent Extended QU-Res. The paper also describes a prototype implementation of the DQRAT-checker incorporating the new rule and discusses further properties of Dpure with potential applications to dependency learning in solvers such as Qute.

Significance. If the p-equivalence result holds, the work would be significant for QBF/DQBF certification by enabling RAT-style checkers to reach the strength of the most powerful known proof systems. The prototype implementation is a concrete practical contribution that moves DQRAT from theory to a usable tool. The additional properties shown for Dpure are noted as potentially useful for solver integration.

major comments (2)
  1. [§3] §3 (Dpure definition): the pure-path formulation must be shown to be a sound dependency scheme for DQBF; without an explicit argument that it neither over- nor under-approximates dependencies on instances with variables shared across quantifier blocks, soundness of the subsequent integration into DQRAT cannot be assessed.
  2. [§5] §5 (p-equivalence proofs): both simulation directions between DQRAT+Dpure and Independent Extended QU-Res are load-bearing for the central claim; the manuscript must supply the explicit reductions or cite the lemmas establishing mutual p-simulation, as any gap directly falsifies the claimed equivalence.
minor comments (1)
  1. [Abstract] The abstract asserts the p-equivalence and implementation but supplies no definitions or proof sketches; a one-sentence pointer to the key technical sections would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. The two major comments identify areas where additional explicit arguments would strengthen the presentation. We address each below and will revise the manuscript to incorporate the requested clarifications.

read point-by-point responses

  1. Referee: [§3] §3 (Dpure definition): the pure-path formulation must be shown to be a sound dependency scheme for DQBF; without an explicit argument that it neither over- nor under-approximates dependencies on instances with variables shared across quantifier blocks, soundness of the subsequent integration into DQRAT cannot be assessed.

    Authors: We agree that an explicit soundness argument is required for Dpure on general DQBF instances, including those with variables shared across quantifier blocks. While the manuscript defines Dpure via pure paths and proceeds to its use in DQRAT, we will add a dedicated lemma in the revised §3 that proves Dpure neither over- nor under-approximates dependencies in such cases, thereby confirming it is a sound dependency scheme. revision: yes

  2. Referee: [§5] §5 (p-equivalence proofs): both simulation directions between DQRAT+Dpure and Independent Extended QU-Res are load-bearing for the central claim; the manuscript must supply the explicit reductions or cite the lemmas establishing mutual p-simulation, as any gap directly falsifies the claimed equivalence.

    Authors: The p-equivalence claim is central and both simulation directions are addressed in §5. To remove any ambiguity, we will expand the section in the revision to include fully explicit reductions for each direction together with direct citations to the supporting lemmas, ensuring the mutual p-simulation is presented without gaps. revision: yes

Circularity Check

0 steps flagged

No circularity: new dependency scheme Dpure introduced with independent proofs

full rationale

The paper defines a new dependency scheme Dpure via pure paths and proves its soundness and simulation properties relative to existing systems like DQRAT and Independent Extended QU-Res. These steps rely on fresh definitions and explicit proof arguments rather than reducing to self-citations, fitted parameters, or prior results by the same authors. The p-equivalence claim is presented as a theorem following from the new rule's addition, with an implementation provided separately; no load-bearing step collapses to a self-referential input by construction. This is a standard theoretical contribution with independent content.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only abstract available; no details on free parameters, axioms or invented entities can be extracted.

pith-pipeline@v0.9.1-grok · 5756 in / 1067 out tokens · 33355 ms · 2026-06-29T00:17:41.565839+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

2 extracted references · 2 canonical work pages

  1. [1]

    URL: https://eprints.whiterose.ac.uk/ id/eprint/162591/,doi:10.1007/s10817-020-09560-1

    Building Strategies into QBF Proofs This is an open access article under the terms of the Creative Commons Attribution 4.0 International (CC BY 4.0) (ht- tps://creativecommons.org/licenses/by/4.0/). URL: https://eprints.whiterose.ac.uk/ id/eprint/162591/,doi:10.1007/s10817-020-09560-1. 8 Olaf Beyersdorff, Joshua Blinkhorn, and Tomáš Peitl. Strong (d)qbf d...

    work page doi:10.1007/s10817-020-09560-1 2020

  2. [2]

    URL:https://drops.dagstuhl

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL:https://drops.dagstuhl. de/entities/document/10.4230/LIPIcs.SAT.2025.25,doi:10.4230/LIPIcs.SAT.2025.25. 45 Luca Pulina and Martina Seidl. The 2016 and 2017 QBF solvers evaluations (qbfeval’16 and qbfeval’17).Artif. Intell., 274:224–248, 2019. URL:https://doi.org/10.1016/j.artint. 2019.04.002,doi:10.10...

    work page doi:10.4230/lipics.sat.2025.25 2025