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