Seminars

Beyond DPLL(T): A new model-based approach to search in SMT and its application to solving nonlinear arithmetic PDF
Clark Barrett, Computer Science Department, New York University

10/5/2012, 2pm, GHC 8102

Abstract

The DPLL(T) architecture, combining a SAT solver with one or more theory solvers, is the state of the art for today's SMT solvers. It works especially well when problems have significant Boolean structure and the theory reasoning required is not too difficult.

However, in cases when the theory reasoning required is significant, the standard DPLL(T) technique may be insufficient. What is needed is a tighter coupling through which the theory solver can help guide the search for a satisfying assignment.

In this talk, I present a new approach developed by my student Dejan Jovanovic together with Leonardo de Moura from Microsoft Research that integrates model-finding, Boolean search, and theory reasoning, and describe how this new approach can be applied to create a remarkably efficient algorithm for solving nonlinear arithmetic.

Biography

Clark Barrett's research interests are propositional satisfiability (SAT), satisfiability modulo theories (SMT), automated deduction and applied logic, proof-producing algorithms, formal and semi-formal verification of hardware and software, combining verification systems.

http://www.cs.nyu.edu/~barrett/