{"@context":"https:\/\/schema.org\/","@type":"ScholarlyArticle","@id":"#article2238","name":"Understanding space in resolution: optimal lower bounds and exponential trade-offs","abstract":"We continue the study of tradeoffs between space and length of\r\nresolution proofs and focus on two new results:\r\n\r\nbegin{enumerate}\r\nitem \r\nWe show that length and space in resolution are uncorrelated. This\r\nis proved by exhibiting families of CNF formulas of size $O(n)$ that\r\nhave proofs of length $O(n)$ but require space $Omega(n \/ log n)$. Our\r\nseparation is the strongest possible since any proof of length $O(n)$\r\ncan always be transformed into a proof in space $O(n \/ log n)$, and\r\nimproves previous work reported in [Nordstr\"{o}m 2006, Nordstr\"{o}m and\r\nH{aa}stad 2008].\r\n\r\nitem We prove a number of trade-off results for space in the range\r\nfrom constant to $O(n \/ log n)$, most of them superpolynomial or even\r\nexponential. This is a dramatic improvement over previous results in\r\n[Ben-Sasson 2002, Hertel and Pitassi 2007, Nordstr\"{o}m 2007].\r\nend{enumerate}\r\n\r\nThe key to our results is the following, somewhat surprising, theorem:\r\n\r\nAny CNF formula $F$ can be transformed by simple substitution\r\ntransformation into a new formula $F'$ such that if $F$ has the right\r\nproperties, $F'$ can be proven in resolution in essentially the same\r\nlength as $F$ but the minimal space needed for $F'$ is lower-bounded\r\nby the number of variables that have to be mentioned simultaneously in\r\nany proof for $F$. Applying this theorem to so-called pebbling\r\nformulas defined in terms of pebble games over directed acyclic graphs\r\nand analyzing black-white pebbling on these graphs yields our results.","keywords":["Proof complexity","Resolution","Pebbling."],"author":[{"@type":"Person","name":"Ben-Sasson, Eli","givenName":"Eli","familyName":"Ben-Sasson"},{"@type":"Person","name":"Nordstr\u00f6m, Jakob","givenName":"Jakob","familyName":"Nordstr\u00f6m"}],"position":6,"pageStart":1,"pageEnd":0,"dateCreated":"2008-12-17","datePublished":"2008-12-17","isAccessibleForFree":true,"license":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode","copyrightHolder":[{"@type":"Person","name":"Ben-Sasson, Eli","givenName":"Eli","familyName":"Ben-Sasson"},{"@type":"Person","name":"Nordstr\u00f6m, Jakob","givenName":"Jakob","familyName":"Nordstr\u00f6m"}],"copyrightYear":"2008","accessMode":"textual","accessModeSufficient":"textual","creativeWorkStatus":"Published","inLanguage":"en-US","sameAs":"https:\/\/doi.org\/10.4230\/DagSemProc.08381.6","publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","isPartOf":{"@type":"PublicationVolume","@id":"#volume717","volumeNumber":8381,"name":"Dagstuhl Seminar Proceedings, Volume 8381","dateCreated":"2008-12-11","datePublished":"2008-12-11","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#article2238","isPartOf":{"@type":"Periodical","@id":"#series119","name":"Dagstuhl Seminar Proceedings","issn":"1862-4405","isAccessibleForFree":true,"publisher":"Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik","hasPart":"#volume717"}}}