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 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\"{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 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.