Cesare Tinelli
University of Iowa

DPLL-based Checkers for Satisfiability Modulo Theories


Satisfiability modulo theories (SMT) is the problem of determining the satisfiability of quantifier-free formulas in the context of a logical theory T of interest.  Like its simpler counterpart, propositional satisfiability (SAT), SMT has applications in circuit design, compiler optimization, software/hardware verification, planning, and scheduling.   For the SAT problem, solvers based of the DPLL method have recently proven extremely successful thanks to the development of very effective search heuristics on top of the basic DPLL.  In this talk, I will discuss a promising approach for adapting both the DPLL method and its heuristics to the SMT case.

I will start by presenting the DPLL method declaratively, as a calculus.   Then I will show that in that formulation the method can be readily extended to a parametrized calculus, DPLL(T), for checking satisfiability modulo any theory T endowed with a "solver", a procedure that decides the satisfiability in T of conjunctions of literals.  As I will illustrate, the new calculus provides a clean theoretical framework for implementing

efficient SMT checkers.   While DPLL(T) is parametrized by just one background theory, many of its potential applications involve the combination of several background theories.  I will then show how a popular method, due to Nelson and Oppen, for combining solvers for signature disjoint theories can be used to easily and cleanly extend the single theory DPLL(T) calculus to a multitheory DPLL(T_1,...,T_n) calculus.

Time permitting, I will conclude by mentioning some recent and very encouraging results obtained with a DPLL(T) implementation developed in collaboration with the Technical University of Catalonia.

Host:  Frank Pfenning
Appointments:  Jennifer Landefeld

Principles of Programming Seminars

Monday, October 4, 2004
3:30 p.m.
Wean Hall 4623