“Satisfiability Modulo Theories” by Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. In Handbook of Satisfiability, Second Edition, vol. 336 of Frontiers in Artificial Intelligence and Applications, (Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, eds.), Feb. 2021, pp. 825-885.
Applications in artificial intelligence and formal verification have greatly benefited from the recent advances in Boolean Satisfiability (SAT). Often, however, applications in these fields require deter- mining the satisfiability of formulas in more expressive logics such as first-order logic. Despite the great progress made in the last twenty years, general-purpose first-order theorem provers (such as provers based on the resolution calculus) are typically not able to solve such formulas directly. The main reason for this is that many applications require not general first-order satisfiability, but rather satisfi- ability with respect to some background theory, which fixes the interpretations of certain predicate and function symbols. For many theories, specialized methods actually yield decision procedures for the satisfiability of quantifier-free formulas or some subclass thereof. This is the case, thanks to classical results in mathematics, for the theory of real numbers and the theory of integer arithmetic (without multiplication). In the last two decades, however, specialized decision procedures have also been discovered for a long and still growing list of other theories with practical applications. These include certain theories of arrays and of strings, several variants of the theory of finite sets or multisets, the theories of several classes of lattices, the theories of finite, regular and infinite trees, 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 (whether they are decision procedures or not) are usually referred to as SMT solvers. This chapter provides a brief overview of SMT and its main approaches, together with references to the relevant literature for a deeper study. In particular, it focuses on the two most successful major approaches so far for implementing SMT solvers, usually referred to as the “eager” and the “lazy” approach. We note that in recent years, ideas from both approaches have been combined in successful solvers, but it is still useful from a pedagogical approach to study them separately.
BibTeX entry:
@incollection{BSST21,
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, Second Edition},
series = {Frontiers in Artificial Intelligence and Applications},
volume = {336},
chapter = {33},
pages = {825--885},
publisher = {IOS Press},
month = feb,
year = {2021},
url = {http://theory.stanford.edu/~barrett/pubs/BSST21.pdf}
}
(This webpage was created with bibtex2web.)