Computer Science Colloquium

A Non-clausal Calculus for Satisfiability Modulo Theories

Cesare Tinelli
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

Directions: http://cs.nyu.edu/csweb/Location/directions.html
Colloquium Information: http://cs.nyu.edu/csweb/Calendar/colloquium/index.html

Hosts:

Clark Barrett barrett@cs.nyu.edu, (212) 998-3105

Abstract

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 structure.

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 formulas.

Bio

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.