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.2016.40
URN: urn:nbn:de:0030-drops-68758
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6875/
Go to the corresponding LIPIcs Volume Portal

Beyersdorff, Olaf ; Chew, Leroy ; Mahajan, Meena ; Shukla, Anil

Understanding Cutting Planes for QBFs

pdf-format:
LIPIcs-FSTTCS-2016-40.pdf (0.5 MB)

Abstract

We define a cutting planes system CP+ForallRed for quantified Boolean formulas (QBF) and analyse the proof-theoretic strength of this new calculus. While in the propositional case, Cutting Planes is of intermediate strength between resolution and Frege, our findings here show that the situation in QBF is slightly more complex: while CP+ForallRed is again weaker than QBF Frege and stronger than the CDCL-based QBF resolution systems Q-Res and QU-Res, it turns out to be incomparable to even the weakest expansion-based QBF resolution system ForallExp+Res.

Technically, our results establish the effectiveness of two lower bound techniques for CP+ForallRed: via strategy extraction and via monotone feasible interpolation.

BibTeX - Entry

@InProceedings{beyersdorff_et_al:LIPIcs:2016:6875,
  author =	{Olaf Beyersdorff and Leroy Chew and Meena Mahajan and Anil Shukla},
  title =	{{Understanding Cutting Planes for QBFs}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{40:1--40:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6875},
  URN =		{urn:nbn:de:0030-drops-68758},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.40},
  annote =	{Keywords: proof complexity, QBF, cutting planes, resolution, simulations}
}

Keywords: proof complexity, QBF, cutting planes, resolution, simulations
Collection: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue Date: 2016
Date of publication: 10.12.2016

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