Satisfiability modulo theories

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

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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
Pages825-885
Number of pages61
Edition1
ISBN (Print)9781586039295
DOIs
StatePublished - Jan 1 2009

Publication series

NameFrontiers in Artificial Intelligence and Applications
Number1
Volume185
ISSN (Print)0922-6389

    Fingerprint

ASJC Scopus subject areas

  • Artificial Intelligence

Cite this

Barrett, C., Sebastiani, R., Seshia, S. A., & Tinelli, C. (2009). Satisfiability modulo theories. In Handbook of Satisfiability (1 ed., pp. 825-885). (Frontiers in Artificial Intelligence and Applications; Vol. 185, No. 1). IOS Press. https://doi.org/10.3233/978-1-58603-929-5-825