Title: Time-Space Tradeoffs in Resolution: Superpolynomial Lower
Bounds for Superlinear Space

Abstract: Either explicitly or implicitly, Resolution is the
underlying method used in the vast majority of systems for SAT solving
and general logical inference.  By storing information derived from
failed searches, modern SAT solvers have vastly increased the size of
problems that can be solved in practice.  We give the first lower
bounds which show that this use of large amounts of space is critical.
In particular, we show that for every polynomial space bound there are
families of problems that have polynomial size Resolution derivations
within that space bound but if the space is reduced by even a small
constant factor no polynomial-sized Resolution derivation exists.

Joint work with Chris Beck and Russell Impagliazzo