Cesare Tinelli

University of
Iowa

DPLL-based Checkers for Satisfiability
Modulo Theories

###

Abstract:

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