Narrow Proofs May Be Maximally Long
Computational Complexity
2014-09-10 v1 Discrete Mathematics
Logic in Computer Science
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^Omega(w). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n^O(w) is essentially tight. Moreover, our lower bound generalizes 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, where the formulas we study have proofs of constant rank and size polynomial in both n and w.
Keywords
Cite
@article{arxiv.1409.2731,
title = {Narrow Proofs May Be Maximally Long},
author = {Albert Atserias and Massimo Lauria and Jakob Nordström},
journal= {arXiv preprint arXiv:1409.2731},
year = {2014}
}