Abstractions in Satisfiability Solvers

Опубликовано 17 августа 2016, 3:25

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.