Talks and Poster Presentations (with Proceedings-Entry):
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.
English 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.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-80223-3_28
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_300330.pdf
Created from the Publication Database of the Vienna University of Technology.