@inproceedings{df914ebeb05d4122b7299d32f2649334,
title = "Narrow proofs may be maximally long",
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.",
keywords = "degree, Lasserre, length, PCR, polynomial calculus, proof complexity, rank, resolution, Sherali-Adams, size, width",
author = "Albert Atserias and Massimo Lauria and Jakob Nordstr{\"o}m",
year = "2014",
doi = "10.1109/CCC.2014.36",
language = "English",
isbn = "9781479936267",
series = "Proceedings of the Annual IEEE Conference on Computational Complexity",
publisher = "IEEE - Institute of Electrical and Electronics Engineers Inc.",
pages = "286--297",
booktitle = "Proceedings - IEEE 29th Conference on Computational Complexity, CCC 2014",
address = "United States",
note = "29th Annual IEEE Conference on Computational Complexity, CCC 2014 ; Conference date: 11-06-2014 Through 13-06-2014",
}