# A Survey of Satisfiability Modulo Theory

arXiv: https://arxiv.org/abs/1606.04786 · HTML: https://mlsanity.com/paper/1606.04786/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Jun 2016.

## Built on by (most cited first, 3 of 3)

- [Autoformulation of Mathematical Optimization Models Using LLMs](https://mlsanity.com/paper/2411.01679/) (2024)
- [Reinforcement Learning with Symbolic Reward Machines](https://mlsanity.com/paper/2603.03068/) (2026)
- [Logic, Optimization, and Artificial Intelligence](https://mlsanity.com/paper/2607.15532/) (2026)

## Abstract (arXiv)

Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.