We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF φ in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of φ requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute φ. These results are best possible (up to a constant factor) and answer questions about space complexity of 3-CNFs.

Space proof complexity for random 3-CNFs / Bennett, Patrick; Bonacina, Ilario; Galesi, Nicola; Huynh, Tony; Molloy, Mike; Wollan, PAUL JOSEPH. - In: INFORMATION AND COMPUTATION. - ISSN 1090-2651. - STAMPA. - (2017), pp. 165-176.

Space proof complexity for random 3-CNFs

GALESI, NICOLA;Huynh, Tony;WOLLAN, PAUL JOSEPH
2017

Abstract

We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF φ in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of φ requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute φ. These results are best possible (up to a constant factor) and answer questions about space complexity of 3-CNFs.
2017
Proof complexity; Polynomial calculus; Monomial space; Random CNFs; Resolution; Total space
01 Pubblicazione su rivista::01a Articolo in rivista
Space proof complexity for random 3-CNFs / Bennett, Patrick; Bonacina, Ilario; Galesi, Nicola; Huynh, Tony; Molloy, Mike; Wollan, PAUL JOSEPH. - In: INFORMATION AND COMPUTATION. - ISSN 1090-2651. - STAMPA. - (2017), pp. 165-176.
File allegati a questo prodotto
File Dimensione Formato  
Galesi_Space_2017.pdf

accesso aperto

Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 403.13 kB
Formato Adobe PDF
403.13 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/978134
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 3
social impact