Abstract

Propositional satisfiability (or SAT) is the problem of determining whether a given propositional formula is satisfied by some assignment of truth values to its variables. "Satisfiability modulo theories" is a strictly more general kind of satisfiability problem concerning the satisfiability of existential first-order formulas in a logical theory T of interest. It is an important kind of satisfiability problem, with applications in such fields as circuit design, compiler optimization, software/hardware verification, planning, and scheduling.
One of the most successful methods for SAT is due to Davis, Putman, Loveland, and Logemann. This method was originally presented, and is still described, procedurally. In this talk, we will abstract most of the control issues of the method and present it instead declaratively as a derivation calculus, the DPLL calculus. We will then describe an extension of DPLL to a new calculus, DPLL(T), for checking satisfiabily modulo a given theory T. The new calculus, parametrized by the theory T, can be used as the basis of novel and efficient implementations of satisfiability checkers for theories with decidable quantifier-free consequences. To support this claim, we will show how several of the most effective techniques currently used to implement fast DPLL-based SAT checkers can be adapted to the implementation of the DPLL(T) calculus.

Dr. Tinelli is an assistant professor of Computer Science at the University of Iowa. He received a PhD and an MS degree in Computer Science from the University of Illinois at Urbana-Champaign, in 1995 and 1999 respectively. His recent 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.