Satisfiability Modulo Theories

Satisfiability Modulo Theories” by Clark Barrett and Cesare Tinelli. In Handbook of Model Checking, (Ed Clarke, Thomas Henzinger, and Helmut Veith, eds.), 2014. In preparation.

Abstract

Satisfiability Modulo Theories (SMT) refers to the problem of determining whether a first-order formula is satisfiable with respect to some logical theory. Solvers based on SMT are used as back-end engines in model checking applications such as bounded, interpolation-based, and predicate abstraction-based model checking. After a brief illustration of these uses, we survey the predominant techniques for solving SMT problems with an emphasis on the lazy approach, in which a propositional satisfiability (SAT) solver is combined with one or more theory solvers. We discuss the architecture of a lazy SMT solver, give examples of theory solvers, show how to combine such solvers modularly, and mention several extensions of the lazy approach.We also briefly describe the eager approach in which the SMT problem is reduced to a SAT problem. Finally, we discuss how the basic framework for determining satisfiability can be extended with additional functionality such as producing models, proofs, unsatisfiable cores, and interpolants.

BibTeX entry:

@incollection{BT14,
   author = {Clark Barrett and Cesare Tinelli},
   editor = {Ed Clarke and Thomas Henzinger and Helmut Veith},
   title = {Satisfiability Modulo Theories},
   booktitle = {Handbook of Model Checking},
   year = {2014},
   note = {In preparation},
   url = {http://www.cs.nyu.edu/~barrett/pubs/BT14.pdf}
}

(This webpage was created with bibtex2web.)