Proof Complexity of Symbolic QBF Reasoning

TL;DR

This paper explores symbolic proof systems for QBF using OBDDs, demonstrating their efficiency for certain formulas and establishing strong lower bounds that are independent of variable orderings.

Contribution

It introduces symbolic proof systems for QBF with OBDDs, showing their advantages and providing new lower bound techniques based on strategy extraction.

Findings

Symbolic QBF proof systems can produce short proofs for formulas with bounded path-width.

Exponential separations are shown between symbolic proof systems and standard clausal proof systems.

New lower bounds are established that are independent of variable ordering and NP-oracles.

Abstract

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.