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

Beyersdorff, Olaf ; Hinde, Luke ; Pich, Ján

Reasons for Hardness in QBF Proof Systems

pdf-format:
LIPIcs-FSTTCS-2017-14.pdf (0.5 MB)

Abstract

We aim to understand inherent reasons for lower bounds for QBF proof systems, and revisit and compare two previous approaches in this direction.

The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we show a refined version of strategy extraction and thereby for any QBF proof system obtain a trichotomy for hardness: (1) via circuit lower bounds, (2) via propositional Resolution lower bounds, or (3) `genuine' QBF lower bounds.

The second approach tries to explain QBF lower bounds through quantifier alternations in a system called relaxing QU-Res (Chen, ICALP'16). We prove a strong lower bound for relaxing QU-Res, which also exhibits significant shortcomings of that model. Prompted by this we propose an alternative, improved version, allowing more flexible oracle queries in proofs. We show that lower bounds in our new model correspond to the trichotomy obtained via strategy extraction.

BibTeX - Entry

@InProceedings{beyersdorff_et_al:LIPIcs:2018:8382,
  author =	{Olaf Beyersdorff and Luke Hinde and J{\'a}n Pich},
  title =	{{Reasons for Hardness in QBF Proof Systems}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Satya Lokam and R. Ramanujam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8382},
  URN =		{urn:nbn:de:0030-drops-83824},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.14},
  annote =	{Keywords: proof complexity, quantified Boolean formulas, resolution, lower bounds}
}

Keywords: proof complexity, quantified Boolean formulas, resolution, lower bounds
Collection: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)
Issue Date: 2018
Date of publication: 12.02.2018

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