2008/01/01 by Eli Ben‐Sasson, Ben-Sasson, Eli, Jakob Nordström +1
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Pebbling. #Proof complexity #Resolution #semigroups and automata theory
paper · doi:10.4230/dagsemproc.08381.6
openalex publication_date 2008/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We continue the study of tradeoffs between space and length of resolution proofs and focus on two new results: beginenumerate 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"om 2006, Nordstr"om and Haastad 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"om 2007]. endenumerate 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.