[Back]

T. Peitl, F. Slivovsky, S. Szeider:
"Proof Complexity of Fragments of Long-Distance Q-Resolution";
Talk: Theory and Application of Satisfiability Testing -- SAT, Lissabon; 2019-07-07 - 2019-07-12; in: "Theory and Applications of Satisfiability Testing - SAT 2019", Lecture Notes in Computer Science, 11628 (2019), ISBN: 978-3-030-24257-2; 319 - 335.

Q-resolution is perhaps the most well-studied proof system
for Quantified Boolean Formulas (QBFs). Its proof complexity is by now
well understood, and several general proof size lower bound techniques
have been developed. The situation is quite different for long-distance
Q-resolution (LDQ-resolution). While lower bounds on LDQ-resolution
proof size have been established for specific families of formulas, we lack
semantically grounded lower bound techniques for LDQ-resolution.
In this work, we study restrictions of LDQ-resolution. We show that a
specific lower bound technique based on bounded-depth strategy extraction
does not work even for reductionless Q-resolution by presenting short
proofs of the QParity formulas. Reductionless Q-resolution is a variant
of LDQ-resolution that admits merging but no universal reduction. We
also prove a lower bound on the proof size of the completion principle
formulas in reductionless Q-resolution. This shows that two natural fragments
of LDQ-resolution are incomparable: Q-resolution, which allows
universal reductions but no merging, and reductionless Q-resolution,
which allows merging but no universal reductions. Finally, we develop
semantically grounded lower bound techniques for fragments of LDQresolution,
specifically tree-like LDQ-resolution and regular reductionless
Q-resolution.

http://dx.doi.org/10.1007/978-3-030-24258-9

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