Abstract Conflict Driven Clause Learning

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.

Speaker Bios

Leopold Haller is currently wrapping up his PhD at Oxford University under the supervision of Daniel Kroening. His focus is on the theory and practice of building more precise static analyses and faster satisfiability solvers by combining ideas from the two fields.

Séries:
Microsoft Research Talks
Date:
Haut-parleurs:
Leopold Haller
Affiliation:
Oxford University

Taille: Microsoft Research Talks