We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n Ω(w) . This shows that the simple counting argument that any formula refutable in width w must have a proof in size n O(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however, where the formulas we study have proofs of constant rank and size polynomial in both n and w.

Narrow proofs may be maximally long / Atserias, Albert; Lauria, Massimo; Nordström, Jakob. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 17:3(2016), pp. 1-30. [10.1145/2898435]

Narrow proofs may be maximally long

LAURIA, MASSIMO;
2016

Abstract

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n Ω(w) . This shows that the simple counting argument that any formula refutable in width w must have a proof in size n O(w) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution (PCR) and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. Our results do not extend all the way to Lasserre, however, where the formulas we study have proofs of constant rank and size polynomial in both n and w.
2016
degree; PCR; polynomial calculus; polynomial calculus resolution; proof complexity; resolution; SAR; Sherali-Adams; Width; theoretical computer science; computer science (all); logic; computational mathematics
01 Pubblicazione su rivista::01a Articolo in rivista
Narrow proofs may be maximally long / Atserias, Albert; Lauria, Massimo; Nordström, Jakob. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 17:3(2016), pp. 1-30. [10.1145/2898435]
File allegati a questo prodotto
File Dimensione Formato  
Atserias_Narrow-Proofs_2016.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 376.55 kB
Formato Adobe PDF
376.55 kB Adobe PDF   Contatta l'autore

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/957459
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 30
  • ???jsp.display-item.citation.isi??? 25
social impact