License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2018.2
URN: urn:nbn:de:0030-drops-85362
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8536/
Go to the corresponding LIPIcs Volume Portal

Mahajan, Meena

Lower Bound Techniques for QBF Proof Systems

pdf-format:
LIPIcs-STACS-2018-2.pdf (0.4 MB)

Abstract

How do we prove that a false QBF is inded 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.

BibTeX - Entry

@InProceedings{mahajan:LIPIcs:2018:8536,
  author =	{Meena Mahajan},
  title =	{{Lower Bound Techniques for QBF Proof Systems}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{2:1--2:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-062-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{96},
  editor =	{Rolf Niedermeier and Brigitte Vall{\'e}e},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8536},
  URN =		{urn:nbn:de:0030-drops-85362},
  doi =		{10.4230/LIPIcs.STACS.2018.2},
  annote =	{Keywords: Proof Complexity, Quantified Boolean formulas, Resolution, Lower Bound Techniques}
}

Keywords: Proof Complexity, Quantified Boolean formulas, Resolution, Lower Bound Techniques
Collection: 35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)
Issue Date: 2018
Date of publication: 27.02.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI