MS Presentation: Nathan Mull

CDCL SAT Solvers, Subsystem of Resolution, and the
Ordered Decision Strategy

Despite the NP-hardness of SAT, algorithms for SAT (SAT solvers) have
become standard tools in industrial settings and are even sometimes
used as NP oracles. Due to their success, there is increased interest
in understanding why they work so well and, moreover, if there is any
theoretical justification for the performance seen in practice. We
consider an approach which relates variants of a particular
algorithmic framework for SAT solving to subsystems of the resolution
proof system. In particular, so-called CDCL solvers, when run on
unsatisfiable formulas, may be thought of as generating proofs of
unsatisfiability, so their refutational strength can be studied using
tools from propositional proof complexity.

We focus on CDCL solvers using a heuristic called the ordered decision
strategy. We prove that such solvers, when also using a heuristic
called the DECISION learning strategy, are not as refutationally
powerful as resolution. We also prove that they become as powerful as
resolution when granted a different learning strategy and
nondeterminism in certain parts of the algorithm. This second results
may be viewed as showing that a natural target for proving separations
between resolution and CDCL solvers with the ordered decision strategy
ultimately fails. To aid the presentation of these results as well as
future work, we present a flexible model and associated notation for
CDCL solvers that allows for succinct and precise theorem statements.

All results are based on joint work with Professor Alexander Razborov
and Shuo Pang.