License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.08381.6
URN: urn:nbn:de:0030-drops-17815
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1781/
Go to the corresponding Portal

Ben-Sasson, Eli ; Nordström, Jakob

Understanding space in resolution: optimal lower bounds and exponential trade-offs

pdf-format:
08381.NordstroemJakob.Paper.1781.pdf (0.5 MB)

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 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.

BibTeX - Entry

@InProceedings{bensasson_et_al:DagSemProc.08381.6,
  author =	{Ben-Sasson, Eli and Nordstr\"{o}m, Jakob},
  title =	{{Understanding space in resolution: optimal lower bounds and exponential trade-offs}},
  booktitle =	{Computational Complexity of Discrete Problems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8381},
  editor =	{Peter Bro Miltersen and R\"{u}diger Reischuk and Georg Schnitger and Dieter van Melkebeek},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2008/1781},
  URN =		{urn:nbn:de:0030-drops-17815},
  doi =		{10.4230/DagSemProc.08381.6},
  annote =	{Keywords: Proof complexity, Resolution, Pebbling.}
}

Keywords: Proof complexity, Resolution, Pebbling.
Collection: 08381 - Computational Complexity of Discrete Problems
Issue Date: 2008
Date of publication: 17.12.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI