BenSasson, Eli ;
Nordström, Jakob
Understanding space in resolution: optimal lower bounds and exponential tradeoffs
Abstract
We continue the study of tradeoffs between space and length of
resolution proofs and focus on two new results:
begin{enumerate}
item
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"{o}m 2006, Nordstr"{o}m and
H{aa}stad 2008].
item We prove a number of tradeoff 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
[BenSasson 2002, Hertel and Pitassi 2007, Nordstr"{o}m 2007].
end{enumerate}
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 lowerbounded
by the number of variables that have to be mentioned simultaneously in
any proof for $F$. Applying this theorem to socalled pebbling
formulas defined in terms of pebble games over directed acyclic graphs
and analyzing blackwhite pebbling on these graphs yields our results.
BibTeX  Entry
@InProceedings{bensasson_et_al:DSP:2008:1781,
author = {Eli BenSasson and Jakob Nordstr{\"o}m},
title = {Understanding space in resolution: optimal lower bounds and exponential tradeoffs},
booktitle = {Computational Complexity of Discrete Problems },
year = {2008},
editor = {Peter Bro Miltersen and R{\"u}diger Reischuk and Georg Schnitger and Dieter van Melkebeek},
number = {08381},
series = {Dagstuhl Seminar Proceedings},
ISSN = {18624405},
publisher = {Schloss Dagstuhl  LeibnizZentrum fuer Informatik, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1781},
annote = {Keywords: Proof complexity, Resolution, Pebbling.}
}
Keywords: 

Proof complexity, Resolution, Pebbling. 
Seminar: 

08381  Computational Complexity of Discrete Problems

Issue date: 

2008 
Date of publication: 

17.12.2008 