An Exponential Time/Space Speedup For Resolution

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 [3] 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 exponenti...

• Type: Journal
• Year: 2007
• Where: ECCC
• Authors: Philipp Hertel, Toniann Pitassi
• Keywords: Backtrack Search Procedure, ECCC 2007, Main, Space