[Proof Complexity] Paper announcement: Narrow Proofs May Be Maximally Long

[Jakob Nordstrom]

Dear colleagues,

A second brief announcement is that we have just posted a full-length version
at http://eccc.hpi-web.de/report/2014/118/ of the paper "Narrow Proofs May Be
Maximally Long" by Albert Atserias, Massimo Lauria, and yours truly. An
extended abstract of this paper appeared at CCC this year.

The abstract follows below. Any comments or questions are more than welcome.

Best regards,
Jakob Nordstrom

**********

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.

Jakob Nordström, Assistant Professor
KTH Royal Institute of Technology
Osquars backe 2, SE-100 44 Stockholm, Sweden
Phone: +46 8 790 69 19 (office), +46 70 742 21 98 (cell)
http://www.csc.kth.se/~jakobn/