Abstractions in Satisfiability Solvers

Speaker  Vijay D'Silva

Host  Josh Berdine

Affiliation  Oxford University

Duration  01:06:38

Date recorded  9 September 2011

Modern satisfiability solvers combine an elegant algorithm with clever heuristics and efficient engineering to achieve extremely high performance. I will show that the Conflict Driven Clause Learning algorithm in modern solvers has a natural characterisation in the framework of abstract interpretation. In particular, SAT solvers operate on a strict abstraction of propositional logic. This is surprising because an imprecise abstraction is used to obtain precise results. Time permitting, I will discuss how one may derive verification algorithms from satisfiability algorithms.

I assume no background in either SAT solving or abstract interpretation.

©2011 Microsoft Corporation. All rights reserved.
> Abstractions in Satisfiability Solvers