Galesi, Nicola ;
Pudlák, Pavel ;
Thapen, Neil
The Space Complexity of Cutting Planes Refutations
Abstract
We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been wellstudied and many optimal linear lower bounds are known.
Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires superconstant space to refute in this system. The system nevertheless already has an exponential speedup over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constantspace cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle.
We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.
BibTeX  Entry
@InProceedings{galesi_et_al:LIPIcs:2015:5055,
author = {Nicola Galesi and Pavel Pudl{\'a}k and Neil Thapen},
title = {{The Space Complexity of Cutting Planes Refutations}},
booktitle = {30th Conference on Computational Complexity (CCC 2015)},
pages = {433447},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897811},
ISSN = {18688969},
year = {2015},
volume = {33},
editor = {David Zuckerman},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5055},
URN = {urn:nbn:de:0030drops50551},
doi = {10.4230/LIPIcs.CCC.2015.433},
annote = {Keywords: Proof Complexity, Cutting Planes, Space Complexity}
}
2015
Keywords: 

Proof Complexity, Cutting Planes, Space Complexity 
Seminar: 

30th Conference on Computational Complexity (CCC 2015)

Issue date: 

2015 
Date of publication: 

2015 