Narrow proofs may be maximally long
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
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.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014 |
Antal sider | 12 |
Forlag | IEEE Computer Society Press |
Publikationsdato | 2014 |
Sider | 286-297 |
Artikelnummer | 6875497 |
ISBN (Trykt) | 9781479936267 |
DOI | |
Status | Udgivet - 2014 |
Eksternt udgivet | Ja |
Begivenhed | 29th Annual IEEE Conference on Computational Complexity, CCC 2014 - Vancouver, BC, Canada Varighed: 11 jun. 2014 → 13 jun. 2014 |
Konference
Konference | 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 |
Navn | Proceedings of the Annual IEEE Conference on Computational Complexity |
---|---|
ISSN | 1093-0159 |
ID: 251870042