“Satisfiability Modulo Theories” by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. In Handbook of Satisfiability, vol. 185 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2009, pp. 825-885.
Applications in artificial intelligence and formal verification have greatly benefited from the recent advances in SAT. It is often the case, however, that applications in these fields require determining the satisfiability of formulas in more expressive logics such as first-order logic. These applications typically require not general first-order satisfiability, but rather satisfiability with respect to some background theory, which fixes the interpretations of certain predicate and function symbols. For many background theories, specialized methods actually yield decision procedures for the satisfiability of quantifier-free formulas or some subclass thereof. Specialized decision procedures have been discovered for a long and still growing list of theories with practical applications. These include the theory of equality, several arithmetic theories, certain theories of arrays and of strings, as well as theories of lists, tuples, records, queues, hash tables, and bit-vectors of a fixed or arbitrary finite size. The research field concerned with the satisfiability of formulas with respect to some background theory is called Satisfiability Modulo Theories, or SMT, for short. In analogy with SAT, SMT procedures are usually referred to as SMT solvers. This chapter provides a brief overview of SMT together with references to the relevant literature for a deeper study. It begins with an overview of techniques for solving SMT by encodings to SAT, known as the “eager” approach. The rest of the chapter is concerned with an alternative technique in which a SAT solver is integrated with a separate decision procedure (called a theory solver) for conjunctions of literals in the theory. This is known as the “lazy” approach. After presenting the lazy approach as a whole, we take a closer look at how to construct theory solvers, how to combinine theory solvers, and several extensions and enhancements.
BibTeX entry:
@incollection{BSST09,
author = {Clark Barrett and Roberto Sebastiani and Sanjit Seshia and
Cesare Tinelli},
editor = {Armin Biere and Marijn J. H. Heule and Hans van Maaren and
Toby Walsh},
title = {Satisfiability Modulo Theories},
booktitle = {Handbook of Satisfiability},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {185},
chapter = {26},
pages = {825--885},
publisher = {IOS Press},
month = feb,
year = {2009},
url = {http://theory.stanford.edu/~barrett/pubs/BSST09.pdf}
}
(This webpage was created with bibtex2web.)