Computer Science/Discrete Mathematics Seminar II

This is joint work with Philipp Hertel 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 {\it 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 \cite{bensasson2002} 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, as well as the related black-white pebbling problem, are PSPACE complete.