Abstraction in Satisfiability Solvers
Vijay D'Silva, Oxford University
- Date and Time
Tuesday, August 23rd, 2011 at 10:30
Polacksbacken, room 1345
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.