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.12
URN: urn:nbn:de:0030-drops-85174
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/8517/
Go to the corresponding LIPIcs Volume Portal

Beyersdorff, Olaf ; Blinkhorn, Joshua

Genuine Lower Bounds for QBF Expansion

pdf-format:
LIPIcs-STACS-2018-12.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{beyersdorff_et_al:LIPIcs:2018:8517,
  author =	{Olaf Beyersdorff and Joshua Blinkhorn},
  title =	{{Genuine Lower Bounds for QBF Expansion}},
  booktitle =	{35th Symposium on Theoretical Aspects of Computer Science (STACS 2018)},
  pages =	{12:1--12:15},
  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/8517},
  URN =		{urn:nbn:de:0030-drops-85174},
  doi =		{10.4230/LIPIcs.STACS.2018.12},
  annote =	{Keywords: QBF, proof complexity, lower-bound techniques, resolution}
}

Keywords: QBF, proof complexity, lower-bound techniques, resolution
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