SMT solving
Satisfiability modulo theories
Abbreviated SMT
Satisfiability with values and operations from stated theories.
Definition
Satisfiability modulo theories
Satisfiability modulo theories (SMT) asks whether constraints have a model under theories such as arithmetic, arrays, strings, or bit-vectors.
SMT preserves structure that plain SAT does not know directly. A solver combines Boolean search with procedures for the selected theories.
01
Example
x > 3 and x < 6 is sat over integers, with x = 4 or x = 5.
02
Important distinction
A logic name states which operations and quantifiers a query may use. Support for one logic does not imply support for every SMT-LIB logic.
After reading this article, you should be able to
- Define SMT in the sense used on this site.
- Explain what SMT adds to Boolean satisfiability.