Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Beyersdorff, Olaf; Chew, Leroy; Mahajan, Meena; Shukla, Anil http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-68758
URL:

; ; ;

Understanding Cutting Planes for QBFs

pdf-format:


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
Seminar: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Issue date: 2016
Date of publication: 2016


DROPS-Home | Fulltext Search | Imprint Published by LZI