University of Cambridge > > Microsoft Research Cambridge, public talks > Abstractions in Satisfiability Solvers

Abstractions in Satisfiability Solvers

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

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.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity