Satisfiability modulo theories

Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, Cesare Tinelli

Research output: Chapter in Book/Report/Conference proceedingChapter


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.

Original languageEnglish (US)
Title of host publicationHandbook of Satisfiability
PublisherIOS Press
Number of pages61
ISBN (Print)9781586039295
StatePublished - 2009

Publication series

NameFrontiers in Artificial Intelligence and Applications
ISSN (Print)0922-6389
ISSN (Electronic)1879-8314

ASJC Scopus subject areas

  • Artificial Intelligence


Dive into the research topics of 'Satisfiability modulo theories'. Together they form a unique fingerprint.

Cite this