Narrow proofs may be maximally long
2014 (English)In: Proceedings of the Annual IEEE Conference on Computational Complexity, 2014, 286-297 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
2014. 286-297 p.
degree, Lasserre, length, PCR, polynomial calculus, proof complexity, rank, resolution, Sherali-Adams, size, width, Calculations, Computational complexity, Optical resolving power, Polynomials
Computer and Information Science
IdentifiersURN: urn:nbn:se:kth:diva-168868DOI: 10.1109/CCC.2014.36ISI: 000345759400028ScopusID: 2-s2.0-84906667234ISBN: 9781479936267OAI: oai:DiVA.org:kth-168868DiVA: diva2:819714
29th Annual IEEE Conference on Computational Complexity, CCC 2014, 11 June 2014 through 13 June 2014, Vancouver, BC
QC 201506112015-06-112015-06-092015-06-11Bibliographically approved