Checking the satisfiability of logical formulas,
SMT solvers scale orders of magnitude beyond
custom ad hoc solvers.
BY LeonaRDo De moURa anD niKoLaJ BJøRneR
Constraint-satisfaction problems arise in diverse
application areas, including software and hardware
verification, type inference, static program analysis,
test-case generation, scheduling, planning, and
graph problems, and share a common trait—a core
component using logical formulas for describing
states and transformations between
them. The most well-known constraint
satisfaction problem is propositional
satisfiability, or SAT, aiming to decide whether a formula over Boolean
variables, formed using logical connectives, can be made true by choosing true/false values for its variables.
Some problems are more naturally
described with richer languages (such
as arithmetic). A supporting theory (of
arithmetic) is then required to capture
the meaning of the formulas. Solvers
for such formulations are commonly
called “satisfiability modulo theories,”
or SMT, solvers.
In the past decade, SMT solvers have
attracted increased attention due to
technological advances and industrial
applications. Yet SMT solvers draw on
some of the most fundamental areas
of computer science, as well as a cen-
tury of symbolic logic. They combine
the problem of Boolean satisfiability
many tools for program analysis, testing,
and verification are based on mathematical
logic as the calculus of computation.
smt solvers are the core engine of many
of these tools.
modern smt solvers integrate
specialized solvers with propositional
satisfiability search techniques.