Paper Info
Title
Are Short Proofs Narrow? QBF Resolution Is Not So Simple.
Abstract
The ground-breaking paper “Short Proofs Are Narrow -- Resolution Made Simple” by Ben-Sasson and Wigderson (J. ACM 2001) introduces what is today arguably the main technique to obtain resolution lower bounds: to show a lower bound for the width of proofs. Another important measure for resolution is space, and in their fundamental work, Atserias and Dalmau (J. Comput. Syst. Sci. 2008) show that lower bounds for space again can be obtained via lower bounds for width. In this article, we assess whether similar techniques are effective for resolution calculi for quantified Boolean formulas (QBFs). There are a number of different QBF resolution calculi like Q-resolution (the classical extension of propositional resolution to QBF) and the more recent calculi ∀Exp+Res and IR-calc. For these systems, a mixed picture emerges. Our main results show that the relations both between size and width and between space and width drastically fail in Q-resolution, even in its weaker tree-like version. On the other hand, we obtain positive results for the expansion-based resolution systems ∀Exp+Res and IR-calc, however, only in the weak tree-like models. Technically, our negative results rely on showing width lower bounds together with simultaneous upper bounds for size and space. For our positive results, we exhibit space and width-preserving simulations between QBF resolution calculi.
Year
DOI
Venue
2018
10.1145/3157053
Electronic Colloquium on Computational Complexity (ECCC)
Keywords
Field
DocType
Proof complexity, QBF, lower bound techniques, resolution, simulations
Discrete mathematics,Combinatorics,Upper and lower bounds,Mathematical proof,Proof complexity,Mathematics
Journal
Volume
Issue
ISSN
19
1
1529-3785
Citations 
PageRank 
References 
4
0.41
30
Authors
4
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Leroy Chew2557.02
Meena Mahajan368856.90
Anil Shukla4131.56