----------------------------------------------------------
    Algorithmic Applications of Propositional Proof Complexity
    ----------------------------------------------------------

Ph.D. Thesis 

Ashish Sabharwal
University of Washington, Seattle

Advisors: Professors Paul Beame and Henry Kautz

ABSTRACT:

This thesis explores algorithmic applications of proof complexity
theory to the areas of exact and approximation algorithms for graph
problems as well as propositional reasoning systems studied commonly
by the artificial intelligence and formal verification communities. On
the theoretical side, our focus is on the propositional proof system
called resolution. On the practical side, we concentrate on
propositional satisfiability algorithms (SAT solvers) which form the
core of numerous real-world automated reasoning systems.

There are three major contributions in this work. (A) We study the
behavior of resolution on appropriate encodings of three graphs
problems, namely, independent set, vertex cover, and clique. We prove
lower bounds on the sizes of resolution proofs for these problems and
derive from this unconditional hardness of approximation results for
resolution-based algorithms. (B) We explore two key techniques used in
SAT solvers called clause learning and restarts, providing the first
formal framework for their analysis. Formulating them as proof
systems, we put them in perspective with respect to resolution and its
refinements. (C) We present new techniques for designing
structure-aware SAT solvers based on high-level problem
descriptions. We present empirical studies which demonstrate that one
can achieve enormous speed-up in practice by incorporating variable
orders as well as symmetry information obtained directly from the
underlying problem domain.