# 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.

- See also unification