__
TR07-046 | 23rd April 2007 00:00
__

#### An Exponential Time/Space Speedup For Resolution

**Abstract:**
Satisfiability algorithms have become one of the most practical and successful approaches for solving a variety of real-world problems, including hardware verification, experimental design, planning and diagnosis problems. The main reason for the success is due to highly optimized algorithms for SAT based on resolution. The most successful of these is clause learning, a DPLL scheme based on caching intermediate clauses that are "learned" throughout the backtrack search procedure. The main bottleneck to this approach is space, and thus there has been a tremendous amount of research aimed at identifying good heuristics for deciding what information to cache. Haken first suggested a formal approach to this issue, and Ben-Sasson posed the question of whether there is a time/space tradeoff for resolution.

Our main result is an optimal time/space tradeoff for resolution. Namely, we present an infinite family of propositional formulas whose minimal space proofs all have exponential time, but if just three extra units of storage are allowed, then the formulas can be proved in linear time.

We also prove another related theorem. Given an unsatisfiable formula F and an integer k, the resolution space problem is to determine if F has a resolution proof which can be verified using space k. We prove that this problem is PSPACE complete.

__
Comment #1 to TR07-046 | 7th October 2007 19:09
__
#### Comments on "An Exponential Time/Space Speedup For Resolution" Comment on: TR07-046

**Abstract:**

We present a greatly simplified proof of the length-space trade-off

result for resolution in Hertel and Pitassi (2007), and point out two

important ingredients needed for our proof to work. Our key trick is

to look at formulas of the type F = G \land H, where G and H are over

disjoint set of variables and have very different length-space

properties with respect to resolution. This trick is not present in

the proof of Hertel and Pitassi, and thus their techniques can likely

be used to prove results not obtainable by our methods.