Department of Information Technology

Abstraction in Satisfiability Solvers

Speaker

Vijay D'Silva, Oxford University

Date and Time

Tuesday, August 23rd, 2011 at 10:30

Location

Polacksbacken, room 1345

Abstract

Contemporary satisfiability solvers for propositional logic and first order theories combine search, deduction, and heuristics to achieve extremely high performance. An important question is how to lift these algorithms to new problem domains. In this talk, I will present a lattice-theoretic analysis of the Conflict Driven Clause Learning algorithm in propositional solvers. I will show that a core component of CDCL is, in a precise, mathematical sense, a standard abstract interpretation procedure. Other components of CDCL are instances of a general method called trace partitioning. This view directly indicates how CDCL can be generalised to richer logics and non-Boolean domains. In fact, the CDCL procedure can be viewed as a novel, property driven refinement technique. Our implementation of this generalised technique is capable of proving properties of highly non-linear programs using simple abstractions. Such proofs are well beyond the scope of existing techniques.

I do not assume background in SAT solving or abstract interpretation and will introduce the relevant aspects of both.

Back to the seminar page

Updated  2011-08-08 14:14:29 by Frédéric Haziza.