Speaker Vijay D'Silva
Host Josh Berdine
Affiliation Oxford University
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.