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

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