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