Propositional Satisfiability to Satisfiability Modulo Theories

Satisfiability Modulo Theories, or SMT, is the problem of deciding the feasibility of a Boolean combination of predicates from one or more background theories, such as the theory of uninterpreted functions, the theory of (integer) linear arithmetic, the theory of arrays, etc. SMT formulas are quite expressive and have numerous applications such as hardware and software verification, scheduling, planning, etc. This talk traces the history of SMT from the original works of Nelson-Oppen and Shostak, which were motivated by program verification, to the present which is witnessing remarkable advances in the performance and scalability of SMT solvers leading to their use in a wider range of applications. The current crop of SMT solvers owe their speed and capacity to the powerful Boolean reasoning capabilities of modern backtrack propositional satisfiability (SAT) solvers. Such solvers augment the classical Davis-Putnam-Logemann-Loveland (DPLL) search algorithm with a variety of techniques that have made it possible to tackle propositional formulas containing tens of thousands of variables and millions of clauses. The architecture of most recent SMT solvers involves a tight integration of specialized theory solvers within a DPLL framework.