> For the complete documentation index, see [llms.txt](https://mandober.gitbook.io/math-debrief/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://mandober.gitbook.io/math-debrief/300-logic/310-mathematical-logic/satisfiability-modulo-theories.md).

# Satisfiability Modulo Theories

<https://en.wikipedia.org/wiki/Satisfiability_modulo_theories>

*The Satisfiability Modulo Theories (SMT) problem* is a decision problem for logical formulas with respect to combinations of background theories expressed in classical FOL with equality.

Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming.