High performance propositional satisfiability solvers based on the Conflict Driven Clause
Learning framework (CDCL) have been a major driver of research in areas such as verification
and decision procedures. Modern satisfiability procedures are routinely applied to problems
that were deemed intractable based on theoretical considerations 15 years ago. Lifting the
algorithmic lessons of CDCL to richer problem domains is a focus of ongoing research.

In this talk, I show how one can generalise CDCL using lattice-theoretic abstractions
to yield natural domain SMT procedures for logics and program verification problems.
I leverage the simple insight that existing CDCL solvers can be characterised as
logical abstract interpreters. The resulting Abstract CDCL (ACDCL) framework is
a mathematical and algorithmic recipe for lifting CDCL by combining over- and
underapproximate abstractions. I discuss the lattice-theoretic prerequisites of
clause learning, give conditions for completeness and present two instantiations
of ACDCL for program verification and SMT problems which significantly outperform
existing techniques.

This talk is based on joint work with Vijay D'Silva, Daniel Kroening, and Alberto Griggio.