S. Mengel, F. Slivovsky:

"Proof Complexity of Symbolic QBF Reasoning";

Talk: International Conference on the Theory and Applications of Satisfiability Testing, Barcelona, Spanien; 2021-07-05 - 2021-07-09; in: "Theory and Applications of Satisfiability Testing - SAT 2021", LNCS / Springer, 12831 (2021), ISBN: 978-3-030-80222-6; 399 - 416.

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.

http://dx.doi.org/10.1007/978-3-030-80223-3_28

https://publik.tuwien.ac.at/files/publik_300330.pdf

Created from the Publication Database of the Vienna University of Technology.