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 PfenningPrinciples
of Programming Seminars