SMT

Satisfiability modulo theories (SMT) generalizes Boolean satisfiability to formulas over richer vocabularies^[1]. An SMT formula may contain integer and real variables with arithmetic, fixed-width bit-vectors with machine operations, arrays with reads and writes, algebraic datatypes, strings, and uninterpreted function symbols, all combined by Boolean connectives. A theory fixes the meaning of these symbols, and the question is whether some assignment satisfies the formula in that theory. SMT solvers answer it by pairing a SAT solver for the Boolean structure with a theory solver for each theory, an arrangement called DPLL(T)^[4]. Leading solvers include Z3, cvc5 and Yices^[2][5][6]. Their common input language, SMT-LIB, and their annual competition have made SMT a standard back end for software and hardware verification^[3].

SMT-LIB defines theories by their signatures and axioms, and logics as fragments of them^[3]. Common logics include QF_UF, quantifier-free formulas with uninterpreted functions, decided by congruence closure; QF_LRA and QF_LIA, linear real and integer arithmetic, decided by variants of the simplex method with branch-and-bound for integers; QF_IDL, integer difference logic; QF_BV, bit-vectors, usually decided by bit-blasting into SAT; and QF_AX, arrays. Formulas mixing theories are handled by Nelson–Oppen combination^[14].

The quantifier-free fragments of these theories are NP-complete, being at least as hard as SAT, although their conjunctions are often polynomial. Nonlinear real arithmetic is decidable, by Tarski's quantifier elimination, and practical solvers use cylindrical algebraic decomposition inside the search^[9]. Nonlinear integer arithmetic is undecidable by Matiyasevich's solution of Hilbert's tenth problem^[15], so solvers for it are incomplete.

Early SMT solvers translated the whole problem to SAT; modern ones are lazy^[1]. The SAT solver treats each theory atom as a propositional variable and searches for an assignment satisfying the Boolean structure. Whenever propagation settles, the theory solvers check the assigned atoms. An inconsistency is reported with an explanation, which the SAT solver learns as a clause, and theory solvers can also report atoms that are implied, which the SAT solver then assigns. Preprocessing simplifies the formula beforehand, eliminating variables, normalizing arithmetic and purifying mixed terms.

(* A tiny SMT solver for integer difference logic (QF_IDL) that reads a
   subset of SMT-LIB: declare-const, assert, check-sat, get-model. *)
type sexp = Atom of string | List of sexp list
 
let parse_all (text : string) : sexp list =
  let toks = ref [] and buf = Buffer.create 16 in
  let flush () = if Buffer.length buf > 0 then (toks := Buffer.contents buf :: !toks; Buffer.clear buf) in
  let in_comment = ref false in
  String.iter (fun ch ->
      if !in_comment then (if ch = '\n' then in_comment := false)
      else match ch with
        | ';' -> flush (); in_comment := true
        | '(' | ')' -> flush (); toks := String.make 1 ch :: !toks
        | ' ' | '\n' | '\t' -> flush ()
        | c -> Buffer.add_char buf c) text;
  flush ();
  let rec sexp = function
    | "(" :: rest -> let items, rest = list rest in (List items, rest)
    | t :: rest -> (Atom t, rest)
    | [] -> failwith "unexpected end"
  and list = function
    | ")" :: rest -> ([], rest)
    | ts -> let s, rest = sexp ts in let items, rest = list rest in (s :: items, rest) in
  let rec all = function [] -> [] | ts -> let s, rest = sexp ts in s :: all rest in
  all (List.rev !toks)
 
(* Boolean structure over difference atoms. A lone variable x stands for
   x - zero, where zero is a variable fixed to 0 in the model. *)
type formula = Lit of Dl.atom | Not of formula | And of formula list | Or of formula list
 
let rec term = function
  | List [ Atom "-"; Atom x; Atom y ] -> (x, y)
  | Atom x -> (x, "zero")
  | _ -> failwith "only x or (- x y) may be compared"
 
let rec formula = function
  | List [ Atom op; lhs; Atom k ] when List.mem op [ "<="; "<"; ">="; ">"; "=" ] ->
    let x, y = term lhs and k = int_of_string k in
    let le x y c = Lit { Dl.x; y; c } in
    (match op with
     | "<=" -> le x y k | "<" -> le x y (k - 1)
     | ">=" -> le y x (-k) | ">" -> le y x (-k - 1)
     | _ -> And [ le x y k; le y x (-k) ])
  | List (Atom "and" :: args) -> And (List.map formula args)
  | List (Atom "or" :: args) -> Or (List.map formula args)
  | List [ Atom "not"; a ] -> Not (formula a)
  | List [ Atom "=>"; a; b ] -> Or [ Not (formula a); formula b ]
  | s -> failwith ("unsupported formula: " ^ (match s with Atom a -> a | _ -> "(...)"))
 
(* Tseitin encoding into clauses. Auxiliary variables are atoms without
   theory content (None), which the theory ignores. *)
let encode (fs : formula list) =
  let atoms = ref [] and n = ref 0 in
  let fresh a = incr n; atoms := a :: !atoms; !n in
  let table = Hashtbl.create 16 in
  let atom a = match Hashtbl.find_opt table a with
    | Some i -> i | None -> let i = fresh (Some a) in Hashtbl.add table a i; i in
  let clauses = ref [] in
  let rec lit = function
    | Lit a -> atom a
    | Not f -> - (lit f)
    | And fs -> let ls = List.map lit fs and g = fresh None in
      List.iter (fun l -> clauses := [ -g; l ] :: !clauses) ls;
      clauses := (g :: List.map (fun l -> -l) ls) :: !clauses; g
    | Or fs -> let ls = List.map lit fs and g = fresh None in
      List.iter (fun l -> clauses := [ g; -l ] :: !clauses) ls;
      clauses := (-g :: ls) :: !clauses; g in
  List.iter (fun f -> let l = lit f in clauses := [ l ] :: !clauses) fs;
  (Array.of_list (List.rev !atoms), !clauses)
 
module Theory = struct
  type atom = Dl.atom option
  type model = (string * int) list
  let check lits =
    match Dl.Theory.check (List.filter_map (fun (a, b) -> Option.map (fun a -> (a, b)) a) lits) with
    | Ok m -> Ok m
    | Error expl -> Error (List.map (fun (a, b) -> (Some a, b)) expl)
end
module S = Dpllt.Make (Theory)
 
(* Run a script, printing the answers to check-sat and get-model. *)
let run (script : string) =
  let decls = ref [] and asserts = ref [] and last = ref None in
  List.iter (function
      | List [ Atom "set-logic"; _ ] -> ()
      | List [ Atom "declare-const"; Atom x; Atom "Int" ] -> decls := !decls @ [ x ]
      | List [ Atom "assert"; f ] -> asserts := !asserts @ [ formula f ]
      | List [ Atom "check-sat" ] ->
        let atoms, clauses = encode !asserts in
        let r, _ = S.solve atoms clauses in
        last := Option.map fst r;
        print_endline (if r = None then "unsat" else "sat")
      | List [ Atom "get-model" ] ->
        (match !last with
         | Some m ->
           let z = try List.assoc "zero" m with Not_found -> 0 in
           print_endline "(";
           List.iter (fun x -> Printf.printf "  (define-fun %s () Int %d)\n" x
                         ((try List.assoc x m with Not_found -> z) - z)) !decls;
           print_endline ")"
         | None -> print_endline "(error \"no model\")")
      | _ -> failwith "unsupported command") (parse_all script)

(* Two jobs of 3 and 4 hours share one machine; the second must start
   within 5 hours of the first. Can both finish by hour 8? by hour 6? *)
let script deadline = Printf.sprintf {|
(set-logic QF_IDL)
(declare-const a Int)   ; start of job A, 3 hours
(declare-const b Int)   ; start of job B, 4 hours
(assert (>= a 0))
(assert (>= b 0))
(assert (or (<= (- a b) -3)      ; A finishes before B starts
            (<= (- b a) -4)))    ; or B finishes before A starts
(assert (<= (- b a) 5))
(assert (<= a %d))
(assert (<= b %d))
(check-sat)
(get-model)
|} (deadline - 3) (deadline - 4)

(set-logic QF_IDL)
(declare-const a Int)   ; start of job A, 3 hours
(declare-const b Int)   ; start of job B, 4 hours
(assert (>= a 0))
(assert (>= b 0))
(assert (or (<= (- a b) -3)      ; A finishes before B starts
            (<= (- b a) -4)))    ; or B finishes before A starts
(assert (<= (- b a) 5))
(assert (<= a 5))
(assert (<= b 4))
(check-sat)
(get-model)
; output:
sat
(
  (define-fun a () Int 0)
  (define-fun b () Int 3)
)
; with a deadline of 6:
unsat
(error "no model")

Formulas with quantifiers, typical of program verification where axioms describe data structures, are undecidable in general. Solvers handle them by instantiation: E-matching instantiates a quantified axiom when ground terms matching a trigger pattern appear in the current assignment^[7], and model-based quantifier instantiation checks a candidate model against each quantified formula and instantiates it with a counterexample if one exists^[8]. Neither is complete, and a solver may answer unknown.

SMT solvers are the reasoning engines of many program analysis tools. Deductive verifiers such as Dafny generate verification conditions from annotated programs and discharge them with Z3^[11]. Symbolic execution tools such as KLEE explore program paths and ask a solver for inputs that follow each path, generating tests^[10]. Refinement type checkers encode subtyping as SMT queries. Amazon Web Services uses SMT solvers to analyze the access-control policies that customers attach to their cloud resources^[12]. Other uses include bounded model checking of hardware and software, scheduling and planning, and program synthesis.

Decision procedures for combinations of theories go back to Nelson and Oppen's cooperating procedures of 1979^[14] and Shostak's method, developed for program verifiers at Stanford and SRI. The Stanford Validity Checker of Barrett, Dill and Levitt in 1996 combined them with case splitting^[13]. Around 2002 several groups coupled decision procedures with SAT solvers lazily, and the DPLL(T) framework of 2004–2006 gave the approach its standard form^[4]. The SMT-LIB initiative began in 2003 to provide a common language and benchmark library, and the SMT competition has been held annually since 2005; version 2.0 of the language, in 2010, introduced the command-based format still used^[3]. Z3 from Microsoft Research, released in 2008, became the most widely used solver^[2], alongside the CVC line, now cvc5^[5], and Yices^[6].

• DPLL(T)DPLL(T) is the architecture of lazy SMT solvers: a CDCL SAT solver searches over the Boolean structure of a formula, treating each theory atom as a propositional variable, and a theory solver for T checks the consistency of the atoms it assigns. When the theory solver finds the assigned literals inconsistent, it returns an explanation, whose negation the SAT solver learns as a clause before backjumping; it may also propagate literals the assignment implies. The approach separates a generic engine from pluggable theory solvers and is used by nearly all SMT solvers, including Z3, cvc5 and Yices.
• Theory solverIn an SMT solver, a theory solver decides whether a conjunction of literals of one theory, such as linear arithmetic or equality with uninterpreted functions, is consistent. The SAT search asserts literals to it incrementally and asks it to check them; on inconsistency it returns an explanation, a small subset of the asserted literals that is already inconsistent, which the SAT search learns as a clause. A theory solver must also undo assertions when the search backtracks, and it may propagate literals that the asserted ones imply. The quality of explanations and propagation largely determines the solver's performance.
• Nelson–Oppen combinationThe Nelson–Oppen method decides satisfiability of quantifier-free formulas that mix several theories with disjoint signatures, such as linear arithmetic and uninterpreted functions, using only a decision procedure for each theory. The formula is first purified, by naming mixed subterms with fresh variables, so that every literal belongs to one theory; the theory solvers then agree on which of their shared variables are equal, either by propagating the equalities each entails (enough for convex theories) or by searching over all arrangements of the shared variables. It is complete for theories that are stably infinite, and it is how SMT solvers combine their theory solvers.
• Congruence closureCongruence closure is the algorithm that decides whether an equation between terms follows from a set of ground equations, using only the laws of equality and the congruence rule that equal arguments give equal function applications. It maintains equivalence classes of subterms in a union–find structure and, whenever two classes merge, merges any applications of the same function whose arguments have become equal. It runs in O(n log n) time and decides the quantifier-free theory of equality with uninterpreted functions (EUF), which makes it a core theory solver in SMT; the same data structure, the e-graph, underlies equality saturation in compilers.
• Difference logicDifference logic is the fragment of linear arithmetic whose atoms bound the difference of two variables by a constant, x − y ≤ c, over the integers or the reals. A conjunction of such constraints is satisfiable exactly when the graph with an edge from y to x of weight c for each constraint has no negative cycle, so it can be decided by shortest-path algorithms such as Bellman–Ford, and a negative cycle is a short explanation of unsatisfiability. Boolean combinations of difference constraints are handled by SMT solvers through DPLL(T); they express scheduling problems and the timing constraints of timed automata.
• SATThe Boolean satisfiability problem, SAT, asks whether some assignment of true and false to the variables of a propositional formula makes the formula true. It was the first problem shown to be NP-complete, so every problem in NP reduces to it, and no polynomial-time algorithm is known. In practice SAT solvers based on conflict-driven clause learning decide industrial instances with millions of variables, which has made SAT a general-purpose engine for hardware and software verification, planning, scheduling and combinatorics.
• Refinement typeA refinement type is a base type paired with a logical predicate that its values must satisfy, such as {v : Int | v > 0}, the positive integers. Type checking generates verification conditions, implications between predicates, and discharges them with an SMT solver, so a program can be checked against preconditions, postconditions and invariants without the programmer writing proof terms. The predicates are restricted to a decidable logic, typically linear arithmetic with uninterpreted functions, which is what keeps checking automatic. LiquidHaskell, F* and Liquid Types are the best-known systems.
• Bit-blastingBit-blasting decides formulas over fixed-width bit-vectors, the machine integers of programs and hardware, by translating every variable into one Boolean variable per bit and every operation into a Boolean circuit, then handing the resulting clauses to a SAT solver. Addition becomes a ripple-carry adder and multiplication a shift-and-add array of adders, encoded with the Tseitin transformation. It is complete and simple, and it is how SMT solvers handle bit-vectors after word-level simplification; its weak point is multiplication, whose circuits are large and hard for SAT solvers.
• Craig interpolationCraig's interpolation theorem states that if a formula A implies a formula B, there is a formula I, the interpolant, built only from the symbols A and B have in common, such that A implies I and I implies B. In verification it is used in the equivalent refutation form: when A ∧ B is unsatisfiable, an interpolant is implied by A, inconsistent with B, and mentions only shared variables. For propositional logic, an interpolant can be computed from a resolution refutation of A ∧ B in linear time, which McMillan used in 2003 to build an unbounded model checker from a SAT solver.
• Simplex methodThe simplex method solves linear programs, maximizing a linear function subject to linear inequalities, by walking along the edges of the feasible polyhedron from vertex to vertex, each step improving the objective, until no neighbouring vertex is better. Each step is a pivot on a tableau. It is fast in practice and in smoothed analysis, but takes exponential time on the Klee-Minty cubes with Dantzig's pivoting rule, and needs a rule such as Bland's to avoid cycling on degenerate problems. Its final tableau also gives a solution of the dual program, certifying optimality.

• Implementing SAT in OCaml Part 3From SAT to SMT: the DPLL(T) architecture, reusing conflict-driven learning for theory conflicts, and a union-find equality theory.
• Implementing SAT in OCaml Part 4A real linear-arithmetic fragment: difference logic atoms x - y <= k, decided by Bellman-Ford negative-cycle detection with explanations.
• Implementing SAT in OCaml Part 5A hand-written C stub binding to Z3, run against the same difference-logic benchmarks as the from-scratch solver, and where it falls over.
• LiquidHaskellRefinement types on real Haskell: measures, refined data, termination, totality, and reading the SMT counterexample when it fails.

1. [1]C. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, “Satisfiability modulo theories”, in A. Biere et al. (eds.), Handbook of Satisfiability, IOS Press (2nd ed., 2021).
2. [2]L. de Moura, N. Bjørner, “Z3: an efficient SMT solver”, TACAS (2008).
3. [3]C. Barrett, P. Fontaine, C. Tinelli, The SMT-LIB Standard, version 2.6 (2017).
4. [4]R. Nieuwenhuis, A. Oliveras, C. Tinelli, “Solving SAT and SAT Modulo Theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T)”, Journal of the ACM 53 (2006).
5. [5]H. Barbosa et al., “cvc5: a versatile and industrial-strength SMT solver”, TACAS (2022).
6. [6]B. Dutertre, “Yices 2.2”, CAV (2014).
7. [7]L. de Moura, N. Bjørner, “Efficient E-matching for SMT solvers”, CADE (2007).
8. [8]Y. Ge, L. de Moura, “Complete instantiation for quantified formulas in satisfiability modulo theories”, CAV (2009).
9. [9]D. Jovanović, L. de Moura, “Solving non-linear arithmetic”, IJCAR (2012).
10. [10]C. Cadar, D. Dunbar, D. Engler, “KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs”, OSDI (2008).
11. [11]K. R. M. Leino, “Dafny: an automatic program verifier for functional correctness”, LPAR (2010).
12. [12]J. Backes et al., “Semantic-based automated reasoning for AWS access policies using SMT”, FMCAD (2018).
13. [13]C. Barrett, D. L. Dill, J. R. Levitt, “Validity checking for combinations of theories with equality”, FMCAD (1996).
14. [14]G. Nelson, D. C. Oppen, “Simplification by cooperating decision procedures”, ACM Transactions on Programming Languages and Systems 1 (1979).
15. [15]Yu. V. Matiyasevich, “Enumerable sets are Diophantine”, Soviet Mathematics Doklady 11 (1970).

last updated 28 September 2026