ECCC-Report TR14-118https://eccc.weizmann.ac.il/report/2014/118Comments and Revisions published for TR14-118en-usTue, 09 Sep 2014 14:42:44 +0300
Paper TR14-118
| Narrow Proofs May Be Maximally Long |
Jakob NordstrÃ¶m,
Albert Atserias,
Massimo Lauria
https://eccc.weizmann.ac.il/report/2014/118We 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.Tue, 09 Sep 2014 14:42:44 +0300https://eccc.weizmann.ac.il/report/2014/118