SAT vs SMT solver, and where theorem provers fit

What does a SAT solver do?

A SAT solver decides whether a propositional formula can be made true. The problem is NP-complete, shown by Stephen Cook in 1971, and yet modern solvers handle formulas with millions of variables. The method descends from the Davis-Putnam procedure of 1960 and the DPLL algorithm of 1962, and today's solvers add conflict-driven clause learning.

SAT suits problems that can be encoded as finite yes-or-no choices, such as hardware checking, scheduling and bounded model checking.

SMT solver: SAT plus theories, with an example

An SMT solver, short for satisfiability modulo theories, combines a SAT engine with decision procedures for specific theories such as integer and real arithmetic, bit vectors, arrays and uninterpreted functions. Problems are commonly written in the SMT-LIB language, and well-known solvers include Z3 and cvc5.

Is Z3 a SAT solver? Not quite: Z3 is an SMT solver that contains a SAT engine at its core. An SMT example is the question whether x + 1 > x holds for every integer x, which needs arithmetic and not just propositional logic. SMT is the workhorse behind many program verifiers and symbolic execution tools, because program conditions mix arithmetic, memory and logic. It handles quantifiers only through heuristics, so it can be incomplete there.

First-order provers: expressive and general

A first-order prover accepts quantified statements over arbitrary function symbols, which is far more expressive than propositional logic. In return it works in a semi-decidable setting, so it may never finish on a non-theorem. Provers such as Vampire, E and iProver use saturation with resolution or superposition, and they can prove statements with quantifier alternations that SMT solvers tend to miss.

Differences between SAT and SMT solvers at a glance

Ask three questions. Is the problem finite and propositional? Use SAT. Does it mix arithmetic or data structures with mostly ground reasoning? Use SMT. Does it rely on general quantified axioms, such as in algebra or set theory? Use a first-order prover.

How they work together

In practice the tools combine. Proof assistants call first-order provers and SMT solvers to close small goals automatically. Some first-order provers use a SAT or SMT solver inside to reason about ground parts of a problem. Annual competitions exist for SAT and for SMT, in addition to CASC, so each class has public benchmarks.