Narrow proofs may be maximally long
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
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.
Original language | English |
---|---|
Title of host publication | Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014 |
Number of pages | 12 |
Publisher | IEEE Computer Society Press |
Publication date | 2014 |
Pages | 286-297 |
Article number | 6875497 |
ISBN (Print) | 9781479936267 |
DOIs | |
Publication status | Published - 2014 |
Externally published | Yes |
Event | 29th Annual IEEE Conference on Computational Complexity, CCC 2014 - Vancouver, BC, Canada Duration: 11 Jun 2014 → 13 Jun 2014 |
Conference
Conference | 29th Annual IEEE Conference on Computational Complexity, CCC 2014 |
---|---|
Land | Canada |
By | Vancouver, BC |
Periode | 11/06/2014 → 13/06/2014 |
Sponsor | Committee on Mathematical, Foundations of Computing, IEEE Computer Society Technical |
Series | Proceedings of the Annual IEEE Conference on Computational Complexity |
---|---|
ISSN | 1093-0159 |
- degree, Lasserre, length, PCR, polynomial calculus, proof complexity, rank, resolution, Sherali-Adams, size, width
Research areas
ID: 251870042