- Author
- Not stated
- Published
- Last edited 30 October 2026
- Kind
- Wikipedia reference article on a logic problem and its solvers
- Original
- en.wikipedia.org/wiki/Satisfiability_modulo_theories
- Subject
- Formal methods and proof
What it is
Volunteer editors wrote this overview. It covers theory, solver architecture, standards and applications. The article says it was first adapted from a column in an ACM newsletter.
What it says
- SMT asks whether a formula is satisfiable under theories such as integers, arrays and strings.
- The article says SMT is typically NP-hard and is undecidable for many theories.
- Early solvers encoded problems as plain SAT. Modern ones pair SAT search with theory solvers.
- Theorem provers favour problems with many quantifiers, while SMT solvers favour large problems without them.
- A table compares many named solvers, such as Z3 and cvc5, by features.
- Listed uses include program verification, symbolic execution, program synthesis and program repair.
- The SMT-LIB standard supports shared benchmarks and a yearly competition called SMT-COMP.
What evidence it gives
The article offers definitions, small example formulas and a solver comparison table. It cites papers and a handbook chapter. It gives no new measurements of its own.
Interests and limits
Volunteers wrote the article and some statements are tagged as needing a citation. The solver table notes that many SMT-LIB entries marked yes may be only partial. The article describes the field and does not rank solvers. It assumes familiarity with logic.