Volume 9 (2013) Article 14 pp. 471-557
Towards an Optimal Separation of Space and Length in Resolution
by
In this paper, we present some evidence indicating that the latter case should hold and provide a roadmap for how such an optimal separation result could be obtained. We do so by proving a tight bound of $\Theta(\sqrt{n})$ on the space needed for so-called pebbling contradictions over pyramid graphs of size $n$. This yields the first polynomial lower bound on space that is not a consequence of a corresponding lower bound on width, as well as an improvement of the weak separation of space and width of Nordström (STOC 2006) from logarithmic to polynomial.