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
Pages825-885
Number of pages61
Volume185
Edition1
DOIs
StatePublished - 2009

Publication series

NameFrontiers in Artificial Intelligence and Applications
Number1
Volume185
ISSN (Print)09226389

Fingerprint

Artificial intelligence
Formal verification

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., Vol. 185, pp. 825-885). (Frontiers in Artificial Intelligence and Applications; Vol. 185, No. 1). https://doi.org/10.3233/978-1-58603-929-5-825

Satisfiability modulo theories. / Barrett, Clark; Sebastiani, Roberto; Seshia, Sanjit A.; Tinelli, Cesare.

Handbook of Satisfiability. Vol. 185 1. ed. 2009. p. 825-885 (Frontiers in Artificial Intelligence and Applications; Vol. 185, No. 1).

Research output: Chapter in Book/Report/Conference proceedingChapter

Barrett, C, Sebastiani, R, Seshia, SA & Tinelli, C 2009, Satisfiability modulo theories. in Handbook of Satisfiability. 1 edn, vol. 185, Frontiers in Artificial Intelligence and Applications, no. 1, vol. 185, pp. 825-885. https://doi.org/10.3233/978-1-58603-929-5-825
Barrett C, Sebastiani R, Seshia SA, Tinelli C. Satisfiability modulo theories. In Handbook of Satisfiability. 1 ed. Vol. 185. 2009. p. 825-885. (Frontiers in Artificial Intelligence and Applications; 1). https://doi.org/10.3233/978-1-58603-929-5-825
Barrett, Clark ; Sebastiani, Roberto ; Seshia, Sanjit A. ; Tinelli, Cesare. / Satisfiability modulo theories. Handbook of Satisfiability. Vol. 185 1. ed. 2009. pp. 825-885 (Frontiers in Artificial Intelligence and Applications; 1).
@inbook{53e486195688442995f82bfe28c55731,
title = "Satisfiability modulo theories",
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.",
author = "Clark Barrett and Roberto Sebastiani and Seshia, {Sanjit A.} and Cesare Tinelli",
year = "2009",
doi = "10.3233/978-1-58603-929-5-825",
language = "English (US)",
isbn = "9781586039295",
volume = "185",
series = "Frontiers in Artificial Intelligence and Applications",
number = "1",
pages = "825--885",
booktitle = "Handbook of Satisfiability",
edition = "1",

}

TY - CHAP

T1 - Satisfiability modulo theories

AU - Barrett, Clark

AU - Sebastiani, Roberto

AU - Seshia, Sanjit A.

AU - Tinelli, Cesare

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=69949133234&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=69949133234&partnerID=8YFLogxK

U2 - 10.3233/978-1-58603-929-5-825

DO - 10.3233/978-1-58603-929-5-825

M3 - Chapter

SN - 9781586039295

VL - 185

T3 - Frontiers in Artificial Intelligence and Applications

SP - 825

EP - 885

BT - Handbook of Satisfiability

ER -