Abstract Conflict Driven Clause Learning

Опубликовано 28 июля 2016, 23:03

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.