Algorithms and Complexity Seminar
Understanding space in resolution: optimal lower bounds and
exponential trade-offs
Jakob Nordström (KTH, MIT)
We continue the study of tradeoffs between space and length of
resolution proofs and focus on two new results:
1) We show that length and space in resolution are uncorrelated. This
is proved by exhibiting families of CNF formulas of size O(n) that
have proofs of length O(n) but require space Omega(n / log n). Our
separation is the strongest possible since any proof of length O(n)
can always be transformed into a proof in space O(n / log n), and
improves previous work reported in [Nordström 2006, Nordström and
Håstad 2008].
2) We prove a number of trade-off results for space in the range from
constant to O(n / log n), most of them superpolynomial or even
exponential. This is a dramatic improvement over previous results in
[Ben-Sasson 2002, Hertel and Pitassi 2007, Nordström 2007].
The key to our results is the following, somewhat surprising, theorem:
Any CNF formula F can be transformed by simple substitution
transformation into a new formula F' such that if F has the right
properties, F' can be proven in resolution in essentially the same
length as F but the minimal space needed for F' is lower-bounded by
the number of variables that have to be mentioned simultaneously in
any proof for F. Applying this theorem to so-called pebbling formulas
defined in terms of pebble games over directed acyclic graphs and
analyzing black-white pebbling on these graphs yields our results.
Joint work with Eli Ben-Sasson.