satisfiability modulo theories
1 General case
What follows is the most general description of SMT that I have come across.
Recall some definitions from Model Theory:
- A sentence is a formula with no free variables
- A theory is a set of sentences
- Given an interpretation a formula has a fixed truth value
If an interpretation can be given that satisfies all sentences of a theory, then the theory is satisfiable.
Automatically finding such interpretations is the aim of an SMT solver.
2 In practice
In practice, we are concerned with formulas that may have un-bound variable. And we are not concerned with just any interpretation structure, but a particular structure, e.g. the integers. After all, many silly interpretations can be found that are consistent with the formula: \[ x > y \wedge x \mod 2 \equiv 0 \] But we are most likely interested in finding numbers that satisfy the formula.