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.