Abstract Conflict Driven Clause Learning

Date

June 28, 2012

Speaker

Leopold Haller

Affiliation

Oxford University

Overview

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.

Speakers

Leopold Haller

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.