Paper Info
Title
Lower Bound Techniques for QBF Proof Systems.
Abstract
How do we prove that a false QBF is indeed false? How big a proof is needed? The special case when all quantifiers are existential is the well-studied setting of propositional proof complexity. Expectedly, universal quantifiers change the game significantly. Several proof systems have been designed in the last couple of decades to handle QBFs. Lower bound paradigms from propositional proof complexity cannot always be extended - in most cases feasible interpolation and consequent transfer of circuit lower bounds works, but obtaining lower bounds on size by providing lower bounds on width fails dramatically. A new paradigm with no analogue in the propositional world has emerged in the form of strategy extraction, allowing for transfer of circuit lower bounds, as well as obtaining independent genuine QBF lower bounds based on a semantic cost measure. This talk will provide a broad overview of some of these developments.
Year
DOI
Venue
2018
10.4230/LIPIcs.STACS.2018.2
Leibniz International Proceedings in Informatics
Keywords
Field
DocType
Proof Complexity,Quantified Boolean formulas,Resolution,Lower Bound Techniques
Discrete mathematics,Upper and lower bounds,Computer science,Interpolation,Proof complexity,Special case
Conference
Volume
ISSN
Citations 
96
1868-8969
0
PageRank 
References 
Authors
0.34
0
1
Name
Order
Citations
PageRank
Meena Mahajan168856.90