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 well-studied 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 super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space 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.

The space complexity of cutting planes refutations / Galesi, Nicola; Pudlák, Pavel; Thapen, Neil. - ELETTRONICO. - 33:(2015), pp. 433-447. (Intervento presentato al convegno 30th Conference on Computational Complexity, CCC 2015 tenutosi a Portrland nel 2015) [10.4230/LIPIcs.CCC.2015.433].

The space complexity of cutting planes refutations

GALESI, NICOLA;
2015

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 well-studied 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 super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space 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.
2015
30th Conference on Computational Complexity, CCC 2015
Cutting planes; Proof complexity; Space complexity; Software
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
The space complexity of cutting planes refutations / Galesi, Nicola; Pudlák, Pavel; Thapen, Neil. - ELETTRONICO. - 33:(2015), pp. 433-447. (Intervento presentato al convegno 30th Conference on Computational Complexity, CCC 2015 tenutosi a Portrland nel 2015) [10.4230/LIPIcs.CCC.2015.433].
File allegati a questo prodotto
File Dimensione Formato  
Galesi_space_2015.pdf

accesso aperto

Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Creative commons
Dimensione 462.25 kB
Formato Adobe PDF
462.25 kB Adobe PDF

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/908272
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 4
social impact