Applications in artificial intelligence, formal verification, and other areas 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. Also, 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 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, various theories of arithmetic, and certain theories of arrays, as well as theories of lists, tuples, records, and bit-vectors of a fixed or arbitrary finite size. The research field concerned with determining the satisfiability of formulas with respect to some background theory is called Satisfiability Modulo Theories (SMT). 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 problems by encodings to SAT. The rest of the chapter is mostly concerned with an alternative approach in which a SAT solver is integrated with a separate decision procedure (called a theory solver) for conjunctions of literals in the background theory. After presenting this approach as a whole, the chapter provides more details on how to construct and combine theory solvers, and discusses several extensions and enhancements.
Effectively Monadic Predicates
