Splitting on Demand in Satisfiability Modulo Theories

November 6, 2006
Cesare Tinelli | University of Iowa

Lazy algorithms for Satisfiability Modulo Theories (SMT) combine a generic DPLL-based SAT engine with a theory solver for a given theory T that can decide the T-consistency of conjunctions of ground literals. For many theories of interest, theory solvers need to reason by performing internal case splits. In this talk we argue that it is more convenient to delegate these case splits to the DPLL engine instead. The delegation can be done on demand for solvers that can encode their internal case splits into one or more clauses, possibly including new constants and literals. This results in drastically simpler theory solvers. We present this splitting-on-demand idea in an extension of Abstract DPLL Modulo Theories, a framework for modeling and reasoning about lazy algorithms for SMT. We also show that splitting-on-demand can be naturally refined to include efficient Nelson-Oppen-like combination of multiple theories and their solvers.

Speaker Details

Cesare Tinelli is an associate professor of Computer Science at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research concentrates on constraint-based approaches and combination methods for automated reasoning, and their applications to software verification and model checking. In 2003, Dr. Tinelli received an NSF CAREER award for a project on improving extended static checking of software by means of advanced automated reasoning techniques. Dr. Tinelli has served in the program committee of several automated reasoning conferences and workshops, such as CADE, LPAR, FroCoS, UNIF, PDPAR, and Disproving, and is currently a steering committee member of CADE, IJCAR, FTP, and FroCoS. He is also the co-leader of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers.