Computer Science Colloquium
A Non-clausal Calculus for Satisfiability Modulo Theories
The University of Iowa
Friday, November 5, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html
Clark Barrett firstname.lastname@example.org, (212) 998-3105
Satisfiability modulo theories (SMT) is the problem of determining the
satisfiability of quantifier-free formulas in the context of a logical
theory of interest. Similarly to 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 on the so-called DPLL method have
been extremely successful thanks to the development of very effective
optimizations and search heuristics over the basic method. While the
DPLL method processes only CNF formulas (as sets of clauses), recent
work has shown that its main ideas and heuristics can be directly applied,
and with great effectiveness, also to formulas with an arbitrary Boolean
Based on this work, in this talk I will present a promising approach for
lifting the DPLL method and its heuristics to the problem of checking the
satisfiability of arbitrary quantifier-free formulas in a given theory.
I will start by presenting declaratively---as a calculus---a non-clausal
propositional version of DPLL. Then I will show that in that formulation
the method can be readily extended to a parametrized calculus for
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 for arbitrary quantifier-free
Dr. Tinelli is an assistant 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 work concentrates
on constraint-based approaches and combination methods for automated
reasoning, and their applications to software verification.
His research interests include automated reasoning, formal methods,
foundations of programming languages, and applications of logic in
computer science. 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.
| contact email@example.com