Clause learning, resolution space, & pebbling

Currently, the most effective complete SAT solvers are based on the DPLL algorithm augmented by Clause Learning. These solvers can handle many real-world problems from application areas like verification, diagnosis, planning, and design. Clause Learning works by storing previously computed, intermediate results and then reusing them to prune the future search tree. Without Clause Learning, however, DPLL loses most of its effectiveness on real world problems. Recently there has been some work on obtaining a deeper understanding of the technique of Clause Learning. In this thesis, we contribute to the understanding of Clause Learning, and the Resolution proof system that underlies it, in a number of ways.;Since Clause Learning makes use of previously derived clauses, it motivates the study of Resolution space. We contribute to this area of study by proving that determining the variable space of a Resolution derivation is PSPACE-complete. The reduction also yields a surprising exponential size/space trade-off for Resolution in which an increase of just 3 units of variable space results in an exponential decrease in proofsize. This result runs counter to the intuitions of many in the SAT-solving community who have generally believed that proof-size should decrease smoothly as available space increases.;In order to prove these Resolution results, we need to make use of some intuition regarding the relationship between Black-White Pebbling and Resolution. In fact, determining the complexity of Resolution variable space required us to first prove that Black-White Pebbling is PSPACE-complete. The complexity of the Black-White Pebbling Game has remained an open problem for 30 years and resisted numerous attempts to solve it. Its solution is the primary contribution of this thesis.;We characterize Clause Learning as a new, intuitive Resolution refinement which we call CL. We then show that CL proofs can effectively p-simulate general Resolution. Furthermore, this result holds even for the more restrictive class of greedy, unit propagating CL proofs, which more accurately characterize Clause Learning as it is used in practice. This result is surprising and indicates that Clause Learning is significantly more powerful than was previously known.