2026-07-23T01:41:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1781 2024-03-06T11:08:19Z ddc:004 open_access

Understanding space in resolution: optimal lower bounds and exponential trade-offs Ben-Sasson, Eli Nordström, Jakob Proof complexity Resolution Pebbling. 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Eli Ben-Sasson and Jakob Nordström 2008 Is Part Of Dagstuhl Seminar Proceedings, Volume 8381, Computational Complexity of Discrete Problems (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.08381.6 urn:nbn:de:0030-drops-17815 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08381.6 eng https://creativecommons.org/licenses/by/4.0/legalcode