[Proof Complexity] Paper announcement: From Small Space to Small Width in Resolution

[Jakob Nordstrom]

Dear colleagues,

This is just to announce (somewhat belatedly) that we have posted a
full-length version at http://eccc.hpi-web.de/report/2014/081/ of the paper
"From Small Space to Small Width in Resolution" by Yuval Filmus, Massimo
Lauria, Mladen Miksa, Marc Vinyals, and myself. A preliminary version appeared
at STACS this year.

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

Best regards,
Jakob Nordstrom

**********

ABSTRACT

In 2003, Atserias and Dalmau resolved a major open question about the
resolution proof system by establishing that the space complexity of CNF
formulas is always an upper bound on the width needed to refute them. Their
proof is beautiful but somewhat mysterious in that it relies heavily on tools
from finite model theory. We give an alternative, completely elementary, proof
that works by simple syntactic manipulations of resolution refutations. As a
by-product, we develop a "black-box" technique for proving space lower bounds
via a "static" complexity measure that works against any resolution
refutation---previous techniques have been inherently adaptive. We conclude by
showing that the related question for polynomial calculus (i.e., whether space
is an upper bound on degree) seems unlikely to be resolvable by similar
methods.


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/