Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Narrow proofs may be maximally long

Atserias, Albert ; Lauria, Massimo and Nordström, Jakob LU (2014) 29th Annual IEEE Conference on Computational Complexity, CCC 2014 In Proceedings of the Annual IEEE Conference on Computational Complexity p.286-297
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 nO(ω) is essentially tight. Moreover, our lower bounds can be generalized 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-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.

Please use this url to cite or link to this publication:
author
; and
publishing date
type
Chapter in Book/Report/Conference proceeding
publication status
published
subject
keywords
degree, Lasserre, length, PCR, polynomial calculus, proof complexity, rank, resolution, Sherali-Adams, size, width
host publication
Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014
series title
Proceedings of the Annual IEEE Conference on Computational Complexity
article number
6875497
pages
12 pages
publisher
IEEE - Institute of Electrical and Electronics Engineers Inc.
conference name
29th Annual IEEE Conference on Computational Complexity, CCC 2014
conference location
Vancouver, BC, Canada
conference dates
2014-06-11 - 2014-06-13
external identifiers
  • scopus:84906667234
ISSN
1093-0159
ISBN
9781479936267
DOI
10.1109/CCC.2014.36
language
English
LU publication?
no
id
df914ebe-b05d-4122-b729-9d32f2649334
date added to LUP
2020-12-18 22:25:15
date last changed
2025-04-04 14:48:33
@inproceedings{df914ebe-b05d-4122-b729-9d32f2649334,
  abstract     = {{<p>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 nO(ω) is essentially tight. Moreover, our lower bounds can be generalized 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-the formulas we study have Lasserre proofs of constant rank and size polynomial in both n and w.</p>}},
  author       = {{Atserias, Albert and Lauria, Massimo and Nordström, Jakob}},
  booktitle    = {{Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014}},
  isbn         = {{9781479936267}},
  issn         = {{1093-0159}},
  keywords     = {{degree; Lasserre; length; PCR; polynomial calculus; proof complexity; rank; resolution; Sherali-Adams; size; width}},
  language     = {{eng}},
  pages        = {{286--297}},
  publisher    = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}},
  series       = {{Proceedings of the Annual IEEE Conference on Computational Complexity}},
  title        = {{Narrow proofs may be maximally long}},
  url          = {{http://dx.doi.org/10.1109/CCC.2014.36}},
  doi          = {{10.1109/CCC.2014.36}},
  year         = {{2014}},
}