Proof Complexity of Symbolic QBF Reasoning
This work addresses the problem of improving proof complexity for QBF reasoning, which is important for automated theorem proving and verification, though it appears incremental as it builds on existing symbolic methods and communication complexity techniques.
The paper introduces symbolic proof systems for Quantified Boolean Formulas using Ordered Binary Decision Diagrams, which capture QBF solvers performing symbolic quantifier elimination and admit short proofs for formulas with bounded path-width and quantifier complexity, resulting in exponential separations from standard clausal proof systems like QU-Resolution and IR-Calc.
We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers that perform symbolic quantifier elimination, and as such admit short proofs of formulas of bounded path-width and quantifier complexity. As a consequence, we obtain exponential separations from standard clausal proof systems, specifically (long-distance) QU-Resolution and IR-Calc. We further develop a lower bound technique for symbolic QBF proof systems based on strategy extraction that lifts known lower bounds from communication complexity. This allows us to derive strong lower bounds against symbolic QBF proof systems that are independent of the variable ordering of the underlying OBDDs, and that hold even if the proof system is allowed access to an NP-oracle.