It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings.
The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers).
Since Boolean satisfiability is already NP-complete, the SMT problem is typically NP-hard, and for many theories it is undecidable.
The resulting decision procedures are often implemented directly in SMT solvers; see, for instance, the decidability of Presburger arithmetic.
Subtheories are also possible: for example, difference logic is a sub-theory of linear arithmetic in which each inequality is restricted to have the form
[citation needed] There is substantial overlap between SMT solving and automated theorem proving (ATP).
For example, an SMT formula allows one to model the datapath operations of a microprocessor at the word rather than the bit level.
Implementing 32-bit integers as bitvectors in answer set programming suffers from most of the same problems that early SMT solvers faced: "obvious" identities such as x+y=y+x are difficult to deduce.
[3] Early attempts for solving SMT instances involved translating them to Boolean SAT instances (e.g., a 32-bit integer variable would be encoded by 32 single-bit variables with appropriate weights and word-level operations such as 'plus' would be replaced by lower-level logic operations on the bits) and passing this formula to a Boolean SAT solver.
This approach, which is referred to as the eager approach (or bitblasting), has its merits: by pre-processing the SMT formula into an equivalent Boolean SAT formula existing Boolean SAT solvers can be used "as-is" and their performance and capacity improvements leveraged over time.
On the other hand, the loss of the high-level semantics of the underlying theories means that the Boolean SAT solver has to work a lot harder than necessary to discover "obvious" facts (such as
[6] Another line of research involves the development of specialized decidable theories, including linear arithmetic over rationals and integers, fixed-width bitvectors,[7] floating-point arithmetic (often implemented in SMT solvers via bit-blasting, i.e., reduction to bitvectors),[8][9] strings,[10] (co)-datatypes,[11] sequences (used to model dynamic arrays),[12] finite sets and relations,[13][14] separation logic,[15] finite fields,[16] and uninterpreted functions among others.
Examples of monotonic theories include graph reachability, collision detection for convex hulls, minimum cuts, and computation tree logic.
However, many real-world systems, such as an aircraft and its behavior, can only be modelled by means of non-linear arithmetic over the real numbers involving transcendental functions.
The first order theory of the natural numbers with addition (but not multiplication), called Presburger arithmetic, is also decidable.
Examples of SMT solvers addressing Boolean combinations of theory atoms from undecidable arithmetic theories over the reals are ABsolver,[20] which employs a classical DPLL(T) architecture with a non-linear optimization packet as (necessarily incomplete) subordinate theory solver, iSAT, building on a unification of DPLL SAT-solving and interval constraint propagation called the iSAT algorithm,[21] and cvc5.
There are multiple attempts to describe a standardized interface to SMT solvers (and automated theorem provers, a term often used synonymously).
The SMT-LIB format also comes with a number of standardized benchmarks and has enabled a yearly competition between SMT solvers called SMT-COMP.
A common technique is to translate preconditions, postconditions, loop conditions, and assertions into SMT formulas in order to determine if all properties can hold.
Boogie is an intermediate verification language that uses Z3 to automatically check simple imperative programs.
Here is a list of mature applications: Many SMT solvers implement a common interface format called SMTLIB2 (such files usually have the extension ".smt2").
The LiquidHaskell tool implements a refinement type based verifier for Haskell that can use any SMTLIB2 compliant solver, e.g. cvc5, MathSat, or Z3.
[citation needed] Example tools in this category include SAGE from Microsoft Research, KLEE, S2E, and Triton.
[citation needed] SMT solvers have been integrated with proof assistants, including Coq[29] and Isabelle/HOL.