Strong (D)QBF Dependency Schemes via Pure Paths with Applications to Proof Checking
For researchers in QBF/DQBF proof complexity and certification, this work provides a missing ingredient to achieve a proof system as strong as the independent extension rule, advancing the state of the art in proof checking.
The paper introduces a new dependency scheme called Dpure, which when added to the DQRAT proof system makes it provably p-equivalent to the most powerful known QBF and DQBF proof systems. The authors implement a prototype checker DQRAT-check and show Dpure's potential in solving and checking.
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.