Paper Info
Title
Genuine Lower Bounds for QBF Expansion.
Abstract
We propose the first general technique for proving genuine lower bounds in expansion-based QBF proof systems. We present the technique in a framework centred on natural properties of winning strategies in the 'evaluation game' interpretation of QBF semantics. As applications, we prove an exponential proof-size lower bound for a whole class of formula families, and demonstrate the power of our approach over existing methods by providing alternative short proofs of two known hardness results. We also use our technique to deduce a result with manifest practical import: in the absence of propositional hardness, formulas separating the two major QBF expansion systems must have unbounded quantifier alternations.
Year
DOI
Venue
2018
10.4230/LIPIcs.STACS.2018.12
Leibniz International Proceedings in Informatics
Keywords
Field
DocType
QBF,Proof Complexity,Lower-bound Techniques,Resolution
Discrete mathematics,Exponential function,Upper and lower bounds,Computer science,Mathematical proof,Semantics
Conference
Volume
ISSN
Citations 
96
1868-8969
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Olaf Beyersdorff122330.33
Joshua Blinkhorn236.16