Existential Quantification as Incremental SAT

Speaker

Jörg Brauer (I11)
Title Existential Quantification as Incremental SAT
When 09.02.2011, 10:00
Where Room 5052
Abstract Elegant ideas and careful engineering have advanced DPLL-based SAT solvers to the state they can rapidly decide the satisfiability of structured problems that involve thousands of variables. SAT has thus been applied to the problem of existential quantifier elimination, yet existing algorithms are considered “inelegant”.

We present an elegant yet efficient algorithm for existential quantifier elimination using incremental SAT solving. The quest for elegance is more than an exercise in aesthetics since existential quantifier elimination finds application in different fields including but not limited to unbounded model checking, predicate abstraction, dependency analysis, information flow analysis, transfer function synthesis and the synthesis of ranking functions. This approach contrasts with existing techniques in that it is based solely on manipulating the SAT instance rather than requiring any reengineering of the SAT solver or needing an auxiliary data structure such as a BDD. The algorithm combines model enumeration with the generation of shortest prime implicants so as to converge onto a quantifier-free formula presented in CNF.
Slides