SMT BookChapter
SMT BookChapter
SMT BookChapter
Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsch
IOS Press, 2008
c 2008 Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia and Cesare Tinelli. All
rights reserved.
Chapter 12
12.1. Introduction
Applications in artificial intelligence and formal methods for hardware and soft-
ware development have greatly benefited from the recent advances in SAT. Often,
however, applications in these fields require determining the satisfiability of for-
mulas in more expressive logics such as first-order logic. Despite the great progress
made in the last twenty years, general-purpose first-order theorem provers (such
as provers based on the resolution calculus) are typically not able to solve such
formulas directly. The main reason for this is that many applications require not
general first-order satisfiability, but rather satisfiability with respect to some back-
ground theory, which fixes the interpretations of certain predicate and function
symbols. For instance, applications using integer arithmetic are not interested
in whether there exists a nonstandard interpretation of the symbols <, +, and 0
that makes the formula
x < y ∧ ¬(x < y + 0)
satisfiable. Instead, they are interested in whether the formula is satisfiable in an
interpretation in which < is the usual ordering over the integers, + is the inte-
ger addition function, and 0 is the additive identity. General-purpose reasoning
methods can be forced to consider only interpretations consistent with a back-
ground theory T , but only by explicitly incorporating the axioms for T into their
input formulas. Even when this is possible,1 the performance of such provers is
often unacceptable. For some background theories, a more viable alternative is
to use reasoning methods tailored to the theory in question. This is particularly
the case for quantifier-free formulas, first-order formulas with no quantifiers but
possibly with variables, such as the formula above.
For many theories, specialized methods actually yield decision procedures for
the satisfiability of quantifier-free formulas or some subclass thereof. This is the
case, because of classical results in mathematics, for the theory of real numbers
and the theory of integer arithmetic (without multiplication). In the last two
1 Some background theories such as the theory of real numbers or the theory of finite trees,
cannot be captured by a finite set of first-order formulas, or, as in the case of the theory of
integer arithmetic (with multiplication), by any decidable set of first-order formulas.
738 Chapter 12. Satisfiability Modulo Theories
decades, however, specialized decision procedures have also been discovered for
a long and still growing list of other theories with practical applications. These
include certain theories of arrays and of strings, several variants of the theory of
finite sets or multisets, the theories of several classes of lattices, the theories of
finite, regular and infinite trees, of lists, tuples, records, queues, hash tables, and
bit-vectors of a fixed or arbitrary finite size.
The research field concerned with the satisfiability of formulas with respect
to some background theory is called Satisfiability Modulo Theories, or SMT, for
short. In analogy with SAT, SMT procedures (whether they are decision proce-
dures or not) are usually referred to as SMT solvers. The roots of SMT can be
traced back to early work in the late 1970s and early 1980s on using decision pro-
cedures in formal methods by such pioneers as Nelson and Oppen [NO80, NO79],
Shostak [Sho78, Sho79, Sho84], and Boyer and Moore [BM90, BM88].2 Modern
SMT research started in the late 1990s with various independent attempts [AG93,
GS96, ACG99, PRSS99, BGV99] to build more scalable SMT solvers by exploit-
ing advances in SAT technology. The last few years have seen a great deal of
interest and research on the foundational and practical aspects of SMT. SMT
solvers have been developed in academia and industry with increasing scope and
performance. SMT solvers or techniques have been integrated into: interactive
theorem provers for high-order logic (such as HOL, Isabelle, and PVS); extended
static checkers (such as Boogie and ESC/Java 2); verification systems (such as
ACL2, Caduceus, SAL, UCLID, and Why); formal CASE environments (such as
KeY); model checkers (such as BLAST, Eureka, MAGIC and SLAM); certifying
compilers (such as Touchstone and TVOC); unit test generators (such as DART,
EXE, CUTE and PEX).
This chapter provides a brief overview of SMT and its main approaches,
together with references to the relevant literature for a deeper study. In particular,
it focuses on the two most successful major approaches so far for implementing
SMT solvers, usually referred to as the “eager” and the “lazy” approach.
The eager approach is based on devising efficient, specialized translations
to convert an input formula into an equisatisfiable propositional formula using
enough relevant consequences of the theory T . The approach applies in principle
to any theory with a decidable ground satisfiability problem, possibly however
at the cost of a significant blow-up in the translation. Its main allure is that
the translation imposes upfront all theory-specific constraints on the SAT solver’s
search space, potentially solving the input formula quickly; in addition, the trans-
lated formula can be given to any off-the-shelf SAT solver. Its viability depends
on the ability of modern SAT solvers to quickly process relevant theory-specific
information encoded into large SAT formulas.
The lazy approach consists in building ad-hoc procedures implementing, in
essence, an inference system specialized on a background theory T . The main
advantage of theory-specific solvers is that one can use whatever specialized al-
gorithms and data structures are best for the theory in question, which typically
leads to better performance. The common practice is to write theory solvers
just for conjunctions of literals—i.e., atomic formulas and their negations. These
2 Notable early systems building on this work are the Boyer-Moore prover, PVS, Simplify,
pared down solvers are then embedded as separate submodules into an efficient
SAT solver, allowing the joint system to accept quantifier-free formulas with an
arbitrary Boolean structure.
The rest of this chapter is structured as follows. Section 12.2 provides back-
ground information, with formal preliminaries and a brief description of a few
theories popular in SMT applications. The next two sections respectively de-
scribe the eager and the lazy approach in some detail. Section 12.5 describes
some general methods for building theory solvers for the lazy approach. Sec-
tion 12.6 focuses on techniques for combining solvers for different theories into a
solvers for a combination of these theories. Finally, Section 12.7, describes some
important extension and enhancements on the methods and techniques described
in the previous sections.
12.2. Background
In this chapter we will work in the context of (classical) first-order logic with
equality (see, e.g., [EFT94, End00]). To make the chapter more self-contained,
however, we introduce here all the relevant basic concepts and notation.
12.2.1.1. Syntax
A signature Σ is set of predicate and function symbols, each with an associated
arity, a non-negative number. For any signature Σ, we denote by ΣF and ΣP
respectively the set of function and of predicate symbols in Σ. We call the 0-
arity symbols of ΣF constant symbols, and usually denote them by the letters a, b
possibly with subscripts. We call the 0-arity symbols of ΣP propositional symbols,
and usually denote them by the letters A, B, possibly with subscripts. Also, we
use f, g, possibly with subscripts, to denote the non-constant symbols of ΣF , and
p, q, possibly with subscripts, to denote the non-propositional symbols of ΣP .
In this chapter, we are mostly interested in quantifier-free terms and formulas
built with the symbols of a given signature Σ. As a technical convenience, we treat
the (free) variables of a quantifier-formula as constants in a suitable expansion of
Σ. For example, if Σ is the signature of integer arithmetic we consider the formula
x < y + 1 as a ground (i.e., variable-free) formula in which x and y are additional
740 Chapter 12. Satisfiability Modulo Theories
12.2.1.2. Semantics
Formulas are given a meaning, that is, a truth value from the set {true, false},
by means of (first-order) models. A model A for a signature Σ, or Σ-model,
is a pair consisting of a non-empty set A, the universe of the model, and a
A
mapping ( ) assigning to each constant symbol a ∈ ΣF an element aA ∈ A,
to each function symbol f ∈ ΣF of arity n > 0 a total function f A : An → A,
to each propositional symbol B ∈ ΣP an element B A ∈ {true, false}, and to
each p ∈ ΣP of arity n > 0 a total function pA : An → {true, false}. This
mapping uniquely determines a homomorphic extension, also denoted as ( )A ,
that maps each Σ-term t to an element tA ∈ A, and each Σ-formula ϕ to an
element ϕA ∈ {true, false}. The extension, which we call an interpretation
of the terms and the formulas, is defined as usual. In particular, for any A:
A A
f (t1 , . . . , tn ) = f A (t1 A , . . . , tn A ); ite(ϕ, t1 , t2 ) equals t1 A if ϕA = true and
t2 A otherwise; p(t1 , . . . , tn )A = pA (t1 A , . . . , tn A ); ⊥A = false; ⊤A = true; and
A 4
(t1 = t2 )A = true iff tA 1 = t2 .
We say that a Σ-model A satisfies (resp. falsifies) a Σ-formula ϕ iff ϕA is true
(resp. false). In SMT, one is not interested in arbitrary models but in models
belonging to a given theory T constraining the interpretation of the symbols of
Σ. Following the more recent SMT literature, we define Σ-theories most generally
as just one or more (possibly infinitely many) Σ-models.5 Then, we say that a
ground Σ-formula is satisfiable in a Σ-theory T , or T -satisfiable, iff there is an
element of the set T that satisfies ϕ. Similarly, a set Γ of ground Σ-formulas
T -entails a ground formula ϕ, written Γ |=T ϕ, iff every model of T that satisfies
3 Note that by allowing propositional symbols in signatures this language properly includes
tified variables, so it is also common to see ground T -validity being described in the literature
as T -validity of universal Σ-formulas.
742 Chapter 12. Satisfiability Modulo Theories
12.2.1.4. Abstraction
For abstraction purposes, we associate with every signature Σ (possibly contain-
ing uninterpreted symbols in the sense above) a signature Ω consisting of the
propositional symbols of Σ plus a set of new propositional symbols having the
same cardinality as the set of ground Σ-atoms. We then fix a bijection T 2B,
called propositional abstraction, between the set of ground Σ-formulas without
ite expressions and the propositional formulas over Ω. This bijection maps each
propositional symbol of Σ to itself and each non-propositional Σ-atom to one of
the additional propositional symbols of Ω, and is homomorphic with respect to
the logical operators.8 The restriction to formulas with no ite’s is without loss of
generality because ite constructs can be eliminated in advance by a satisfiability-
preserving transformation that repeatedly applies the following rule to comple-
tion: let ite(ψ, t1 , t2 ) be a subterm appearing in a formula ϕ; we replace this term
in ϕ by some new uninterpreted constant a and return the conjunction of the
result with the formula ite(ψ, a = t1 , a = t2 ). 9 We denote by B2T the inverse of
T 2B, and call it refinement.
To streamline the notation we will often write ϕp to denote T 2B(ϕ). Also,
if µ is a set of Σ-formulas, we will write µp to denote the set {ϕp | ϕ ∈ µ}; if
µp is a set of Boolean literals, then µ will denote B2T (µp ). A Σ-formula ϕ is
propositionally unsatisfiable if ϕp |= ⊥. We will often write µ |=p ϕ to mean
µp |= ϕp . We point out that for any theory T , µ |=p ϕ implies µ |=T ϕ, but not
vice versa.
12.2.2.1. Equality
As described above, a theory usually imposes some restrictions on how function
or predicate symbols may be interpreted. However, the most general case is a
theory which imposes no such restrictions, in other words, a theory that includes
all possible models for a given signature.
7 We refer the reader to, e.g., [EFT94] for a definition of isomorphic models. Intuitively,
two models A and B are isomorphic if they are identical with the possible exception that the
universe of B is a renaming of the universe of A.
8 That is, T 2B(⊥) = ⊥, T 2B(ϕ ∧ ϕ ) = T 2B(ϕ ) ∧ T 2B(ϕ ), and so on.
1 2 1 2
9 The newly-introduced ite can be thought of as syntactic sugar for ψ → a = t ∧¬ψ → a = t .
1 2
Alternatively, to avoid potential blowup of the formula, a formula-level if-then-else operator can
be introduced into the language syntax.
10 See [MZ03a] for an earlier related survey.
Chapter 12. Satisfiability Modulo Theories 743
Given any signature, we denote the theory that includes all possible models of
that theory as T E . It is also sometimes called the empty theory because its finite
axiomatization is just ∅ (the empty set). Because no constraints are imposed
on the way the symbols in the signature may be interpreted, it is also sometimes
called the theory of equality with uninterpreted functions (EUF). The satisfiability
problem for conjunctions of ground formulas modulo T E is decidable in polynomial
time using a procedure known as congruence closure [BTV03, DST80, NO05b].
Some of the first applications that combined Boolean reasoning with theory
reasoning used this simple theory [NO80]. Uninterpreted functions are often used
as an abstraction technique to remove unnecessarily complex or irrelevant details
of a system being modeled. For example, suppose we want to prove that the
following set of literals is unsatisfiable: {a ∗ (f (b) + f (c)) = d, b ∗ (f (a) + f (c)) 6=
d, a = b}. At first, it may appear that this requires reasoning in the theory of
arithmetic. However, if we abstract + and ∗ by replacing them with uninterpreted
functions g and h respectively, we get a new set of literals: {h(a, g(f (b), f (c))) =
d, h(b, g(f (a), f (c))) 6= d, a = b}. This set of literals can be proved unsatisfiable
using only congruence closure.
12.2.2.2. Arithmetic
Let ΣZ be the signature (0, 1, +, −, ≤). Let the theory T Z consist of the model
that interprets these symbols in the usual way over the integers.11 This theory is
also known as Presburger arithmetic.12 We can define the theory T R to consist
of the model that interprets these same symbols in the usual way over the reals.
Let T ′Z be the extension of T Z with an arbitrary number of uninterpreted
constants (and similarly for T ′R ). The question of satisfiability for conjunctions
of ground formulas in either of these theories is decidable. Ground satisfiabil-
ity in T ′R is actually decidable in polynomial time [Kar84], though exponential
methods such as those based on the Simplex algorithm often perform best in
practice (see, e.g. [DdM06b]). On the other hand, ground T ′Z -satisfiability is
NP-complete [Pap81].
Two important related problems have to do with restricting the syntax of
arithmetic formulas in these theories. Difference logic formulas require that every
atom be of the form a − b ⊲⊳ t where a and b are uninterpreted constants, ⊲⊳
is either = or ≤, and t is an integer (i.e. either a sum of 1’s or the negation
of a sum of 1’s). Fast algorithms for difference logic formulas have been studied
in [NO05c]. A slight variation on difference logic is UTVPI (“unit two variable per
inequality”) formulas which in addition to the above pattern also allow a + b ⊲⊳ t.
Algorithms for UTVPI formulas have been explored in [LM05, SS05].
An obvious extension of the basic arithmetic theories discussed so far is to
add multiplication. Unfortunately, this dramatically increases the complexity of
the problem, and so is often avoided in practice. In fact, the integer case becomes
11 Of course, additional symbols can be included for numerals besides 0 and 1 or for <, >, and
≥, but these add no expressive power to the theory, so we omit them for the sake of simplicity.
12 In Presburger arithmetic, the domain is typically taken to be the natural numbers rather
than the integers, but it is straightforward to translate a formula with integer variables to one
where variables are interpreted over N and vice-versa by adding (linearly many) additional
variables or constraints.
744 Chapter 12. Satisfiability Modulo Theories
undecidable even for conjunctions of ground formulas [Mat71]. The real case is
decidable but is doubly-exponential [DH88].
There are obviously many practical uses of decision procedures for arithmetic
and solvers for these or closely related theories have been around for a long time.
In particular, when modeling and reasoning about systems, arithmetic is useful for
modeling finite sets, program arithmetic, manipulation of pointers and memory,
real-time constraints, physical properties of the environment, etc.
12.2.2.3. Arrays
Let ΣA be the signature (read , write ). Given an array a, the term read (a, i)
denotes the value at index i of a and the term write (a, i, v) denotes an array that
is identical to a except that the value at index i is v. More formally, let ΛA be
the following axioms:
Then the theory T A of arrays is the set of all models of these axioms. It is
common also to include the following axiom of extensionality:
We will denote the resulting theory T Aex . The satisfiability of ground formulas
over T ′A or T ′Aex is NP-complete, but various algorithms have been developed that
work well in practice [SJ80, Opp80a, Lev99, SDBL01, BMS06]. Theories of arrays
are commonly used to model actual array data structures in programs. They are
also often used as an abstraction for memory. The advantage of modeling memory
with arrays is that the size of the model depends on the number of accesses to
memory rather than the size of the memory being modeled. In many cases, this
leads to significant efficiency gains.
cons and null, selectors car and cdr, and testers is cons and is null. The first
order signature of an IDT associates a function symbol with each constructor
and selector and a predicate symbol with each tester. The standard model for
such a signature is a term model built using only the constructors. For IDTs
with a single constructor, a conjunction of literals is decidable in polynomial time
using an algorithm by Oppen [Opp80a]. For more general IDTs, the problem is
NP complete, but reasonbly efficient algorithms exist in practice [BST07]. IDTs
are very general and can be used to model a variety of things, e.g., enumerations,
records, tuples, program data types, and type systems.
The eager approach to SMT solving involves translating the original formula to
an equisatisfiable Boolean formula in a single step. In order to generate a small
SAT problem, several optimizations are performed in this translation. As one
might expect, some optimizations are computationally expensive and thus there
is a trade-off between the degree of optimization performed and the amount of
time spent therein. In fact, the translation procedure is much like an optimizing
compiler, with the “high-level program” being the original SMT problem and the
“low-level object code” being the generated SAT problem. This section describes
the main ideas in the eager approach and surveys the state of the art.
12.3.1. Overview
The translations used in the eager approach are, by their very nature, theory-
specific. We survey here the transformations for a combination of two theories:
T E and T Z . These theories, plus an extension of the basic syntax to include
restricted lambda expressions (see below), form the core logic of the original
UCLID decision procedure [LS04a, Ses05], which is the main tool implementing
the eager approach. The UCLID logic has sufficed for a range of applications,
from microprocessor design verification [LB03] to analyzing software for security
vulnerabilities [Ses05].
As mentioned, the theories of interest for this section are T E and T Z , with
signatures as given in §12.2.2. In particular, we assume a signature Σ containing
0, 1, +, −, ≤, and any number of uninterpreted functions and predicates.
Lambda expressions. For additional expressiveness, in this section we consider
an extension of the core logical syntax (as given in Figure 12.1) to include lambda
expressions. Assuming an infinite set V of integer variables, the extended syntax
is given in Figure 12.2.
Notice that the use of lambda expressions is quite restricted. In particular,
there is no way in the logic to express any form of iteration or recursion. An
integer variable x is said to be bound in expression E when it occurs inside a
lambda expression for which x is one of the argument variables. We say that an
expression is well-formed when it contains no unbound variables.
Satisfiability and entailment are defined for well-formed formulas just as
in §12.2.1 for formulas without lambdas. Well-formed formulas containing lamb-
das are considered to be semantically equivalent to their beta-reduced forms
(see §12.3.1.2, below), which do not contain lambdas.
746 Chapter 12. Satisfiability Modulo Theories
Lambda notation allows us to model the effect of a sequence of read and write
operations on a memory (the select and update operations on an array) without the
added complexity of the theory of arrays (T A ). At any point of system operation,
a memory can be represented by a function expression M denoting a mapping
from addresses to values (for an array, the mapping is from indices to values).
The initial state of the memory is given by an uninterpreted function symbol m0
indicating an arbitrary memory state. The effect of a write operation with terms
A and D denoting the address and data values yields a function expression M ′ :
Reading from array M at address A simply yields the function application M (A).
Multi-dimensional memories or arrays are easily expressed in the same way.
Moreover, lambda expressions can express parallel-update operations, which up-
date multiple memory locations in a single step. The details are outside the scope
of this chapter, and can be found elsewhere [Ses05].
12.3.1.1. Operation
Suppose that we are given a formula Forig in the syntax of Figure 12.2 We de-
cide the satisfiability of Forig by performing a three-stage satisfiability-preserving
translation to a Boolean formula Fbool , and then invoking a SAT solver on Fbool .
The three stages of translation are as follows:
1. All lambda expressions are eliminated, resulting in a formula Fnorm . This
stage is described in §12.3.1.2.
2. Function and predicate applications of non-zero arity are eliminated to get
a formula Farith . This stage is described in §12.3.1.3.
3. Formula Farith is a quantifier-free linear integer arithmetic (ΣZ -) formula.
There is more than one way to translate Farith to an equisatisfiable Boolean
formula Fbool . We describe these techniques in §12.3.2–§12.3.4.
Chapter 12. Satisfiability Modulo Theories 747
12.3.1.4. Summary
We conclude this section with observations on the worst-case blow-up in formula
size in going from the starting formula Forig to the quantifier-free arithmetic
formula Farith . The lambda elimination step can result in a worst-case exponential
blow-up, but is typically only linear. In going from the lambda-free formula Fnorm
to Farith , the worst-case blow-up is only quadratic. Thus, if the result of lambda
expansion is linear in the size of Forig , Farith is at most quadratic in the size of
Forig .
We next consider the two main classes of methods for transforming Farith to
an equisatisfiable Boolean formula Fbool : the small-domain encoding method and
the direct encoding method.
The formula Farith is a quantifier-free ΣZ -formula, and so, we are concerned with
T Z -satisfiability of quantifier-free ΣZ -formulas. Recall that this problem is NP-
complete (as discussed in 12.2.2). In the remainder of this section, we assume
satisfiability is with respect to T Z and that all formulas are quantifier-free ΣZ -
formulas.
A formula is constructed by combining linear constraints with Boolean oper-
ators (such as ∧, ∨, ¬). Formally, the ith constraint is of the form
n
X
ai,j xj ≥ bi
j=1
where the coefficients and the constant terms are integer constants and the vari-
ables13 x1 , x2 , . . . , xn are integer-valued.
If there is a satisfying solution to a formula, there is one whose size, measured
in bits, is polynomially bounded in the problem size [BT76, vzGS78, KM78,
Pap81]. Problem size is traditionally measured in terms of the parameters m,
n, log amax , and log bmax , where m is the total number of constraints in the
formula, n is the number of variables (integer-valued constant symbols), and
amax = max(i,j) |ai,j | and bmax = maxi |bi | are the maximums of the absolute
values of coefficients and constant terms respectively.
The above result implies that we can use an enumerative approach to deciding
the satisfiability of a formula, where we restrict our search for satisfying solutions
to within the bound on the problem size mentioned above. This approach is
referred to as the small-domain encoding (SD) method.
In this method, given a formula FZ , we first compute the polynomial bound
S on solution size, and then search for a satisfying solution to FZ in the bounded
13 Constant symbols denoting unknown integer values are called “variables” in this section as
it is the more common term used in literature on solving integer linear arithmetic constraints.
750 Chapter 12. Satisfiability Modulo Theories
12.3.2.1. Equalities
When all linear constraints are equalities (or disequalities) over integer variables,
the fragment of T Z is called equality logic. For this fragment, we have the following
“folk theorem” that is easily obtained:
The key proof argument is that any satisfying assignment can be translated
to the range {0, 1, 2, . . . , n − 1}, since we can only tell whether variable values
differ, not by how much.
This bound yields a search space of size O(nn ), which can be far too large
in many cases. Several optimizations are possible. The most obvious is to divide
the set of variables into equivalence classes so that two variables that appear in
the same equality fall into the same class. Then a separate bound on solution size
can be derived for each equivalence class. This optimization is clearly applicable
for arbitrary linear constraints, not just equalities.
The range allocation method [PRSS02] is another effective technique for re-
ducing the size of the search space. This method operates by first building a
constraint graph representing equalities and disequalities between variables in
the formula, with separate types of edges representing equalities and disequalities
in the negation normal form. Connected components of this graph correspond to
equivalence classes mentioned above. Furthermore, the only major restriction on
satisfying solutions comes from cycles that contain exactly one disequality edge.
Pnueli et al. [PRSS02] give a graph-based algorithm that assigns, to each variable
that participates in both equality and disequality constraints, a set of values large
enough to consider all possible legal truth assignments to the constraints contain-
ing it. The resulting set of values assigned to each variable can be of cardinality
smaller than n, thus often resulting in a more compact search space than nn .
However, the worst case solution size is still n, and the search space can still be
Θ(nn ).
Theorem 12.3.4. Let Futvpi be a UTVPI formula with n variables. Let bmax
be the maximum over the absolute values of all constraints in Futvpi . Then,
752 Chapter 12. Satisfiability Modulo Theories
The theorem can be proved using results from polyhedral theory [Ses05,
SSB07]. A UTVPI formula can be viewed as a union of polyhedra defined by
UTVPI hyperplanes. The vertices of these polyhedra are half-integral. The main
step in the proof is to show that if a satisfying solution exists (i.e., there is an
integer point inside some polyhedron in the union), then there is a solution that
can be obtained by rounding some vertex of a polyhedron in the union. Since
the above bound works for the vertices of the UTVPI polyhedra, it suffices for
searching for integer solutions also.
The most general case is when no restricting assumptions can be made on the
structure of linear constraints. In this case, we can still improve the “typical-
case” complexity of SAT-encoding by exploiting the structure of constraints that
appear in practical problems of interest.
It has been observed [Ses05, Pra77, DNS03] that formulas arising in software
verification have:
Seshia and Bryant [SB05] exploited above special structure to obtain a bound on
solution size that is parameterized in terms of k and w in addition to m, n, amax
and bmax . Their main result is stated in the following theorem.
12.3.2.5. Summary
Table 12.1 summarizes the value of d for all the classes of linear constraints
explored in this section. We can clearly see that the solution bound for arbitrary
Table 12.1. Solution bounds for classes of linear constraints. The classes are listed top
to bottom in increasing order of expressiveness.
the number of transitivity constraints is small and the resulting SAT problem is
easily solved. Various heuristic optimizations are possible based on the Boolean
structure of the formula [Str02b].
Strichman [Str02a] also extended the above scheme to operate on an arbitrary
linear arithmetic formula (over the integers or the rationals). The “transitivity
constraints” are generated using the Fourier-Motzkin variable elimination proce-
dure (the Omega test variant [Pug91], in the case of integers). It is well-known
that Fourier-Motzkin can generate doubly-exponentially many new constraints in
the worst case [Cha93]. Thus, the worst-case size of Fcons is doubly-exponential
in the size of Farith . This worst-case behavior does seem to occur in practice, as
evidenced by the results in Strichman’s paper [Str02a] and subsequent work.
We summarize the complexity of the direct encoding method for the three
classes of linear arithmetic formulas in Table 12.2.
Table 12.2. Worst-case size of direct encoding. The classes are listed top to bottom in
increasing order of expressiveness.
In §12.3.2 and §12.3.3, we have introduced two very distinct methods of deciding
a linear arithmetic formula via translation to SAT. This naturally gives rise to the
following question: Given a formula, which encoding technique should one use to
decide that formula the fastest? This question is an instance of the automated
algorithm selection problem.
On first glance, it might seem that the small-domain encoding would be best,
since it avoids the potential exponential or doubly-exponential blowup in SAT
problem size that the direct encoding can suffer in the worst case. However, this
blowup is not always a problem because of the special structure of the generated
SAT instance. The form of a transitivity constraint is b1 ∧ b2 =⇒ b3 where
b1 , b2 , b3 are Boolean variables encoding linear constraints. If the polarities of
these variables are chosen appropriately, the resulting constraint is either a Horn
constraint or can be transformed into one by variable renaming. Thus, the overall
SAT encoding is a “mostly-HornSAT” problem: i.e., the vast majority of clauses
are Horn clauses. It has been observed for difference logic that the generated SAT
problems are solved quickly in practice in spite of their large size [Ses05].
The question on the choice of encoding has been studied in the context of
difference logic [Ses05]. It has been found that this question cannot be resolved
entirely in favor of either method. One can select an encoding method based
on formula characteristics using a rule generated by machine learning from past
examples (formulas) [SLB03, Ses05]. Moreover, parts of a single formula cor-
responding to different variable classes can be encoded using different encoding
Chapter 12. Satisfiability Modulo Theories 755
methods. The resulting hybrid encoding algorithm has been empirically shown
to be more robust to variation in formula characteristics than either of the two
techniques in isolation [Ses05]. This hybrid algorithm is the first successful use of
automated algorithm selection based on machine learning in SMT solvers.
The alternative to the eager approach, as described above, is the lazy approach
in which efficient SAT solvers are integrated with decision procedures for first-
order theories (also called Theory Solvers or T -solvers) [AG93, WW99, ACG99,
dMRS02, ABC+ 02, BDS02a, GHN+ 04, NO05c, YM06]). Systems based on
this approach are called lazy SMT solvers, and include ArgoLib [MJ04], Ario
[SS05], Barcelogic [NO05a], CVC3 [BT07], Fx7 [ML06], ICS [FORS01], Math-
SAT [BBC+ 05a], Simplify [DNS03], TSAT++ [ACGM04], Verifun [FJOS03],
Yices [DdM06a], and Z3 [dMB08].
In its simplest form, a theory solver for a theory T (T -solver) is a procedure which
takes as input a collection of T -literals µ and decides whether µ is T -satisfiable. In
order for a T -solver to be effectively used within a lazy SMT solver, the following
features are often important or even essential. In the following, we assume an
SMT solver has been called on a T -formula ϕ.
Model generation: when the T -solver is invoked on a T -consistent set µ, it is
able to produce a T -model I witnessing the consistency of µ, i.e., I |=T µ.
Conflict set generation: when the T -solver is invoked on a T -inconsistent set
µ, it is able to produce the (possibly minimal) subset η of µ which has
caused its inconsistency. η is called a theory conflict set of µ.D
Incrementality: the T -solver “remembers” its computation status from one
call to the next, so that, whenever it is given as input a set µ1 ∪µ2 such that
µ1 has just been proved T -satisfiable, it avoids restarting the computation
from scratch.
Backtrackability: it is possible for the T -solver to undo steps and return to a
previous state in an efficient manner.
Deduction of unassigned literals: when the T -solver is invoked on a T -con-
sistent set µ, it can also perform deductions of the form η |=T l, where
η ⊆ µ and l is a literal on a not-yet-assigned atom in ϕ.14
Deduction of interface equalities: when returning Sat, the T -solver canWalso
perform deductions of the form µ |=T e (if T is convex) or µ |=T j ej
(if T is not convex) where e, e1 , ..., en are equalities between variables or
terms occurring in atoms in µ. We call such equalities interface equalities
and denote the interface equality (vi = vj ) by eij . Deductions of inter-
face equalities are also called eij -deductions. Notice that here the deduced
equalities need not occur in the input formula ϕ.
14 Notice that, in principle, every T -solver has deduction capabilities, as it is always possible
to call T -solver(µ∪{¬l}) for every unassigned literal l [ACG99]. We call this technique plunging
[DNS03]. In practice, plunging is very inefficient.
756 Chapter 12. Satisfiability Modulo Theories
Different variants of lazy SMT procedures have been presented. Here we consider
variants in which the Boolean abstraction ϕp of the input formula ϕ is fed into
a DPLL-based SAT solver (henceforth referred to as a DPLL solver). Note that
since most DPLL solvers accept only CNF, if ϕp has arbitrary Boolean structure,
it is first converted into an equisatisfiable CNF formula using standard techniques
(see §2).
In its simplest integration schema [BDS02a, dMRS02], sometimes called “off-
line” [FJOS03],15 the Boolean abstraction ϕp of the input formula is fed to a
DPLL solver, which either decides that ϕp is unsatisfiable, and hence ϕ is T -
unsatisfiable, or it returns a satisfying assignment µp ; in the latter case, the set
of literals µ corresponding to µp is given as input to the T -solver. If µ is found
to be T -consistent, then ϕ is T -consistent. If not, ¬µp is added as a clause to
ϕp , and the SAT solver is restarted from scratch on the resulting formula. Notice
that here DPLL is used as a black-box.
In a more sophisticated schema [AG93, GS96, ACG99, WW99, ABC+ 02,
FJOS03, GHN+ 04, BBC+ 06], called “online” [FJOS03], DPLL is modified to
work directly as an enumerator of truth assignments, whose T -satisfiability is
checked by a T -solver. This schema evolved from that of the DPLL-based proce-
dures for modal logics (see §25.3 and §25.4). Figure 12.3 shows an online T -DPLL
procedure based on a modern DPLL engine [ZMMM01, ZM02]. The inputs ϕ
and µ are a T -formula and a reference to an (initially empty) set of T -literals
respectively. The DPLL solver embedded in T -DPLL reasons on and updates
15 The offline approach is also called the “lemmas on demand” approach in [dMRS02].
Chapter 12. Satisfiability Modulo Theories 757
ϕp and µp , and T -DPLL maintains some data structure encoding the set Lits(ϕ)
and the bijective mapping T 2B/B2T on literals.16
T -preprocess simplifies ϕ into a simpler formula, and updates µ if necessary,
so as to preserve the T -satisfiability of ϕ ∧ µ. If this process produces some
conflict, then T -DPLL returns Unsat. T -preprocess combines most or all of
the Boolean preprocessing steps of DPLL with some theory-dependent rewriting
steps on the T -literals of ϕ. (The latter are described in §12.4.3.1. and §12.4.3.2.)
T -decide next branch selects the next literal to split on as in standard
DPLL (but it may also take into consideration the semantics in T of the literals
being selected.)
T -deduce, in its simplest version, behaves similarly to standard BCP in
DPLL: it iteratively deduces Boolean literals lp implied by the current assignment
(i.e., s.t. ϕp ∧ µp |=p lp , “|=p ” being propositional entailment) and updates ϕp
and µp accordingly, until one of the following conditions occur:
(i) µp propositionally violates ϕp (µp ∧ ϕp |=p ⊥). If so, T -deduce behaves like
deduce in DPLL, returning Conflict.
(ii) µp propositionally satisfies ϕp (µp |=p ϕp ). If so, T -deduce invokes the
T -solver on µ: if the latter returns Sat, then T -deduce returns Sat; other-
wise, T -deduce returns Conflict.
(iii) no more literals can be deduced. If so, T -deduce returns Unknown. A slightly
more elaborate version of T -deduce can invoke the T -solver on µ also at this
intermediate stage: if the T -solver returns Unsat, then T -deduce returns
Conflict. (This enhancement, called early pruning, is discussed in §12.4.3.3.)
A much more elaborate version of T -deduce can be implemented if the T -solver
is able to perform deductions of unassigned literals. (This enhancement, called
T -propagation, is discussed in §12.4.3.4.)
T -analyze conflict is an extension of the analyze conflict algorithm
found in many implementations of DPLL [ZMMM01, ZM02]: if the conflict
produced by T -deduce is caused by a Boolean failure (case (i) above), then
T -analyze conflict produces a Boolean conflict set η p and the corresponding
value of blevel; if instead the conflict is caused by a T -inconsistency revealed by
T -solver (case (ii) or (iii) above), then the result of T -analyze conflict is the
Boolean abstraction η p of the theory conflict set η ⊆ µ produced by the T -solver,
or a mixed Boolean+theory conflict set computed by a backward-traversal of the
implication graph starting from the conflicting clause ¬η p (see §12.4.3.5). If the
T -solver is not able to return a theory conflict set, the whole assignment µ may
be used, after removing all Boolean literals from µ. Once the conflict set η p and
blevel have been computed, T -backtrack behaves analogously to backtrack
in DPLL: it adds the clause ¬η p to ϕp , either temporarily or permanently, and
backtracks up to blevel. (These features, called T -backjumping and T -learning,
are discussed in §12.4.3.5.)
T -DPLL differs from the DPLL schema of [ZMMM01, ZM02] because it
exploits:
16 We implicitly assume that all functions called in T -DPLL have direct access to Lits(ϕ) and
to T 2B/B2T , and that both T 2B and B2T require constant time for mapping each literal.
758 Chapter 12. Satisfiability Modulo Theories
ϕ= ϕp =
c1 : {¬(2x2 − x3 > 2) ∨ A1 } {¬B1 ∨ A1 } ¬B5
c2 : {¬A2 ∨ (x1 − x5 ≤ 1)} {¬A2 ∨ B2 }
c3 : {(3x1 − 2x2 ≤ 3) ∨ A2 } {B3 ∨ A2 } B8
c4 : {¬(2x3 + x4 ≥ 5) ∨ ¬(3x1 − x3 ≤ 6) ∨ ¬A1 } {¬B4 ∨ ¬B5 ∨ ¬A1 } B6
c5 : {A1 ∨ (3x1 − 2x2 ≤ 3)} {A1 ∨ B3 } ¬B2
c6 : {(x2 − x4 ≤ 6) ∨ (x5 = 5 − 3x4 ) ∨ ¬A1 } {B6 ∨ B7 ∨ ¬A1 } ¬B1
c7 : {A1 ∨ (x3 = 3x5 + 4) ∨ A2 } {A1 ∨ B8 ∨ A2 }
¬A2
¬B3 T B3
A1
A2
B2
c8 : B5 ∨ ¬B8 ∨ ¬B2
Figure 12.4. Boolean search (sub)tree in the scenario of Example 12.4.1. (A diagonal line, a
vertical line and a vertical line tagged with “T ” denote literal selection, unit propagation and
T -propagation respectively; a bullet “•” denotes a call to the T -solver.)
Example 12.4.1. Consider the formulas ϕ and ϕp shown in Figure 12.4. Suppose
T -decide next branch selects, in order, µp := {¬B5 , B8 , B6 , ¬B1 } (in c4 , c7 , c6 ,
and c1 ). T -deduce cannot unit-propagate any literal. Assuming the enhanced
version of step (iii), it invokes the T -solver on µ := {¬(3x1 − x3 ≤ 6), (x3 =
3x5 + 4), (x2 − x4 ≤ 6), ¬(2x2 − x3 > 2)}. Suppose the enhanced T -solver not only
returns Sat, but also deduces ¬(3x1 − 2x2 ≤ 3) (c3 and c5 ) as a consequence of the
first and last literals. The corresponding Boolean literal ¬B3 , is then added to µp
and propagated (T -propagation). As a result, A1 , A2 and B2 are unit-propagated
from c5 , c3 and c2 .
Let µ′p be the resulting assignment {¬B5 , B8 , B6 , ¬B1 , ¬B3 , A1 , A2 , B2 }).
By step (iii), T -deduce invokes the T -solver on µ′ : {¬(3x1 − x3 ≤ 6), (x3 =
3x5 + 4), (x2 − x4 ≤ 6), ¬(2x2 − x3 > 2), ¬(3x1 − 2x2 ≤ 3), (x1 − x5 ≤ 1)} which
is inconsistent because of the 1st, 2nd, and 6th literals. As a result, the T -solver
returns Unsat, and hence T -deduce returns Conflict. Next, T -analyze conflict
and T -backtrack learn the corresponding Boolean conflict clause
and backtrack, popping from µp all literals up to {¬B5 , B8 }, and then unit-
propagating ¬B2 on c8 (T -backjumping and T -learning). Then, starting from
{¬B5 , B8 , ¬B2 }, ¬A2 and B3 are also unit-propagated (on c2 and c3 respectively).
Chapter 12. Satisfiability Modulo Theories 759
We describe some of the most effective techniques which have been proposed in
order to optimize the interaction between the DPLL solver and the T -solver. (We
refer the reader to [Seb07] for a much more extensive and detailed survey.) Some
of them derive from those developed in the context of DPLL-based procedures
for modal logics (see §25.4.1).
Intuitively, one can think of static learning as suggesting some small and
“obvious” T -valid lemmas relating some T -atoms of ϕ, which drive DPLL in its
Boolean search. Notice that, unlike the extra clauses added in “per-constraint”
eager approaches [SSB02, SLB03] (see §12.3), the clauses added by static learn-
ing refer only to atoms which already occur in the original formula, so that the
Boolean search space is not enlarged. Notice also that these clauses are not
needed for correctness or completeness: rather, they are used only for pruning
the Boolean search space.
12.4.3.4. T -propagation
As discussed in §12.4.1, for some theories it is possible to implement the T -solver
so that a call to T -solver(µ) returning Sat can also perform one or more deduc-
tion(s) of the form η |=T l, where η ⊆ µ and l is a literal on an unassigned atom
in ϕ. If this is the case, then the T -solver can return l to T -DPLL, so that lp is
added to µp and unit-propagated [ACG99, ABC+ 02, GHN+ 04, NO05c]. This pro-
cess, which is called T -propagation,18 may result in new literals being assigned,
leading to new calls to the T -solver, followed by additional new assignments being
deduced, and so on, so that together, T -propagation and unit propagation may
produce a much larger benefit than either of them alone. As with early-pruning,
there are different strategies by which T -propagation can be interleaved with unit-
propagation [ACG99, ABC+ 02, GHN+ 04, BBC+ 05a, NO05c, CM06a, NOT06].
Notice that when the T -solver deduces η |=T l, it can return this deduction
to T -DPLL, which can then add the T -deduction clause (η p → lp ) to ϕp , either
temporarily or permanently. The T -deduction clause can be used during the rest
of the search, with benefits analogous to those of T -learning (see §12.4.3.5).
As with static learning, the clauses added by T -learning refer only to atoms
which already occur in the original formula, so that no new atom is added.
[FJOS03] proposed an interesting generalization of T -learning, in which learned
clause may contain also new atoms. [BBC+ 05c, BBC+ 06] used a similar idea to
improve the efficiency of Delayed Theory Combination (see §12.6.3). [WGG06]
762 Chapter 12. Satisfiability Modulo Theories
proposed similar ideas for a SMT tool for difference logic, in which new atoms
can be generated selectively according to an ad-hoc heuristic.
must be dropped not only from the assignment, but also from the list of literals which can be
T -deduced, so that to avoid the T -propagation of literals which have been filtered away.
20 Also called triggering in [WW99, ABC+ 02].
Chapter 12. Satisfiability Modulo Theories 763
The DPLL procedure and its variants and extensions, including T -DPLL, can
also be described more abstractly as transition systems. This allows one to ignore
unimportant control and implementation details and provide the essence of each
variant in terms of a set of state transition rules and a rule application strategy.
Following the Abstract DPLL Modulo Theories framework first introduced
in [NOT05], the variants of T -DPLL discussed in the previous subsection can be
described abstractly as a transition relation over states of the form Fail or µ || ϕ,
where ϕ is a (ground) CNF formula, or, equivalently, a finite set of clauses, and
µ is a sequence of (ground) literals, each marked as a decision or a non-decision
literal. As in §12.4.1, the set µ represents a partial assignment of truth values to
the atoms of ϕ. The transition relation is specified by a set of transition rules,
given below. In the rules, we denote the concatenation of sequences of literals
by simple juxtaposition (e.g., µ µ′ µ′′ ), treating single literals as one element
sequences and denoting the empty sequence with ∅. To denote that a literal l
is annotated as a decision literal in a sequence we write it as l• . A literal l is
undefined in µ if neither l nor ¬l occurs in µ. We write S =⇒ S ′ as usual to
mean that two states S and S ′ are related by the transition relation =⇒ and say
that there is a transition from S to S ′ . We call any sequence of transitions of the
form S0 =⇒ S1 =⇒ S2 =⇒ . . . a derivation.
Definition 12.4.3 (Transition Rules). The following is a set of rules for Abstract
T -DPLL. Except for Decide, all the rules that introduce new literals annotate
them as non-decision literals.
µ |=p ¬c
Propagate : µ || ϕ, c ∨ l =⇒ µ l || ϕ, c ∨ l if
l is undefined in µ
• l or ¬l occurs in ϕ
Decide : µ || ϕ =⇒ µ l || ϕ if
l is undefined in µ
µ |=p ¬c
Fail : µ || ϕ, c =⇒ Fail if
µ contains no decision literals
Restart : µ || ϕ =⇒ ∅ || ϕ
µ |=T l
T -Propagate : µ || ϕ =⇒ µ l || ϕ if l or ¬l occurs in ϕ
l is undefined in µ
each atom of c occurs in µ || ϕ
T -Learn : µ || ϕ =⇒ µ || ϕ, c if
ϕ |=T c
T -Forget : µ || ϕ, c =⇒ µ || ϕ if ϕ |=T c
T -Backjump : • ′
µ l µ |=p ¬c, and there is
some clause c′ ∨ l′ such that:
µ l• µ′ || ϕ, c =⇒ µ k || ϕ, c if ϕ, c |=T c′ ∨ l′ and µ |=p ¬c′ ,
l′ is undefined in µ, and
l or ¬l occurs in µ l• µ′ || ϕ
764 Chapter 12. Satisfiability Modulo Theories
The clauses c and c′ ∨l′ in the T -Backjump rule are respectively the conflicting
clause and the backjump clause of the rule.
The rules Propagate, Decide, Fail and Restart, operate at the propositional
level. The other rules involve the theory T and have rather general preconditions.
While all of these preconditions are decidable whenever the T -satisfiability of
sets of ground literals is decidable, they might be expensive to check in their
full generality.21 However, there exist restricted applications of these rules that
are both efficient and enough for completeness [NOT06]. Given a ground CNF
formula ϕ, the purpose of the rules above is to extend and modify an originally
empty sequence until it determines a total, satisfying assignment for ϕ or the Fail
rule becomes applicable.
Example 12.4.4. The computation discussed in Example 12.4.2 can be described
by the following derivation in Abstract T -DPLL, where ϕ is again the formula
consisting of the T R -clauses c1 , . . . , c7 in Figure 12.4 and c8 is the clause ab-
stracted by B5 ∨ ¬B8 ∨ ¬B2 . For space constraints, instead of ϕ’s literals we use
their propositional abstraction here, and use =⇒+ to denote multiple transitions.
1−4. ∅ || ϕ =⇒+ ¬B5 • B8 • B6 • ¬B1 • || ϕ (by Decide)
5. =⇒ ¬B5 • B8 • B6 • ¬B1 • ¬B3 || ϕ (by T -Propagate)
6−8. =⇒+ ¬B5 • B8 • B6 • ¬B1 • ¬B3 A1 A2 B2 || ϕ (by Propagate)
9. =⇒ ¬B5 • B8 • B6 • ¬B1 • ¬B3 A1 A2 B2 || ϕ, c8 (by T -Learn)
10. =⇒ ¬B5 • B8 • B1 || ϕ, c8 (by T -Backjump)
11. =⇒ ¬B5 • B8 • B1 A1 || ϕ, c8 (by Propagate)
applies to l or its negation. This is intentional since such control considerations are best left to
a rule application strategy.
766 Chapter 12. Satisfiability Modulo Theories
T -Learn. This rule allows the addition to the current formula ϕ of an arbitrary
clause c that is T -entailed by ϕ and consists of atoms in the current state. It
can be used to model the static learning techniques described in §12.4.3.2 as well
as the usual conflict-driven lemma learning that adds backjump clauses, or any
other technique that takes advantage of theory consequences of ϕ. In particular,
it can be used to model uniformly all the early pruning techniques described in
§12.4.3.3. This is because any backjumping motivated by the T -inconsistency
of the current assignment µ can be modeled as the discovery and learning of a
theory lemma c that is propositionally falsified by µ, followed by an application of
T -Backjump with c as the conflicting clause. The rule does not model the learning
of clauses containing new literals, which is done by some SMT solvers, as seen in
§12.4.3.5. An extension of Abstract T -DPLL that allows that is dicussed later
in §12.5.2.
We can now describe some of the approaches for implementing T -DPLL solvers
discussed in §12.4.2 in terms of Abstract T -DPLL. (See [NOT06] for more de-
tails.)
Offline integrations of a theory solver and a DPLL solver are modeled by a
class of rule application strategies that do not use the T -Propagate rule. Whenever
a strategy in this class produces a state µ || ϕ irreducible by Decide, Fail, Propagate,
or T -Backjump, the sequence µ is a satisfying assignment for the formula ϕ0 in
the initial state ∅ || ϕ0 , but it may not be T -consistent. If it is not, there exists
a η ⊆ µ such that ∅ |=T ¬η. The strategy then adds the theory lemma ¬η
(the blocking clause) with one T -Learn step and applies Restart, repeating the
same cycle above until a T -compatible state is generated. With an incremental
T -solver it might be more convenient to check the T -consistency of µ in a state
µ || ϕ even if the state is reducible by one of the four rules above. In that case,
it is possible to learn a blocking clause and restart earlier. Strategies like these
are sound and complete. To be fair, and so terminating, they must not remove
(with T -Forget) any blocking clause.
A strategy can take advantage of an online SAT-solver by preferring back-
jumping to systematic restarting after µ is found T -inconsistent. This is done by
first learning a lemma ¬η for some η ⊆ µ, and then repairing µ using that lemma.
In fact, since ¬η is a conflicting clause by construction, either T -Backjump or Fail
applies—depending respectively on whether µ contains decision literals or not. To
be fair, strategies that apply T -Backjump/Fail instead of Restart do not need to
keep the blocking clause once they use it as the conflicting clause for backjumping.
Any fair strategy above remains fair if it is modified to interleave arbitrary
applications of T -Propagate. Stronger results are possible if T -Propagate is ap-
plied eagerly (in concrete, if it has higher priority than Decide). In that case, it
is impossible to generate T -inconsistent assignments, and so it is unnecessary for
correctness to learn any blocking clauses, or any theory lemmas at all.
The lazy approach to SMT as described above relies on combining a SAT solver
with a theory solver for some theory T . The role of the theory solver is to accept a
Chapter 12. Satisfiability Modulo Theories 767
set of literals and report whether the set is T -satisfiable or not. Typically, theory
solvers are ad hoc, with specialized decision procedure tailored to the theory in
question. For details on such procedures for some common theories, we refer
the reader to the references given in §12.2.2. Because different theories often
share some charactaristics, a natural question is whether there exist general or
parameterized methods that have broader applicability. This section discusses
several such approaches that have been developed: Shostak’s method (§12.5.1),
splitting on demand (§12.5.2), layered theory solvers (§12.5.3), and rewriting-
based theory solvers (§12.5.4).
Shostak’s method was introduced in a 1984 paper [Sho84] as a general method for
combining the theory of equality with one or more additional theories that satisfy
certain specific criteria. The original paper lacks rigor and contains serious errors,
but work since then has shed considerable light on the original claims [CLS96,
RS01, SR02, KC03, BDS02b, Gan02]. We summarize some of the most signifiant
results here. We start with some definitions.
Figure 12.5. Algorithm S1: A simple satisfiability checker based on Shostak’s algorithm
The main result in Shostak’s paper is that given a Shostak theory T , a simple
algorithm can be used to determine the satisfiability of conjunctions of Σ-literals.
Algorithm S1 (shown in Figure 12.5) makes use of the properties of a Shostak
theory to check the joint satisfiability of an arbitrary set of equalities, Γ, and an
arbitrary set of disequalities, ∆, in a Shostak theory with canonizer canon and
solver solve.
Algorithm S1 is sound and complete whenever ∆ contains at most one dis-
equality or if T satisfies the additional requirement of being convex (as defined
in §12.2.1.2).
′
Example 12.5.4. Perhaps the most obvious example of a Shostak theory is TR .
A simple canonizer for this theory can be obtained by imposing an order on all
ground constants and combining like terms. For example, canon(c+ 3b − a− 5c) ≡
−a + 3b + (−4c). Similarly, a solver can be obtained simply by solving for one
of the constants in an equation (returning ⊥ if no solution exists). For this
theory, Algorithm S1 corresponds to Gaussian elimination with back-substitution.
Consider the following set of literals: {a+3b−2c = 1, a−b−6c = 1, b+a 6= a−c}.
The following table shows the values of Γ, S, s∗ = t∗ , and S ∗ on each iteration
of Algorithm S1 starting with Γ = {a + 3b − 2c = 1, a − b − 6c = 1}:
Γ S s ∗ = t∗ S∗
a + 3b − 2c = 1 ∅ a + 3b − 2c = 1 a = 1 − 3b + 2c
a − b − 6c = 1
a − b − 6c = 1 a = 1 − 3b + 2c 1 − 3b + 2c − b − 6c = 1 b = −c
∅ a = 1 + 5c
b = −c
Thus far, we have assumed that a theory solver T -solver for a theory T takes as
input a set of literals and outputs true if the set is T -consistent and false otherwise.
For some important theories, determining the T -consistency of a conjunction of
literals requires internal case splitting (i.e. case splitting within the T -solver).
Because theories like T A require internal case splits, solving problems with gen-
eral Boolean structure over such theories using the framework developed in §12.4
results in a system where case splitting occurs in two places: in the Boolean DPLL
(SAT) engine as well as inside the theory solver. In order to simplify the imple-
mentation of theory solvers for such theories, and to centralize the case splitting
in a single part of the system, it is desirable to allow a theory solver T -solver to
demand that the DPLL engine do additional case splits before determining the
T -consistency of a partial assignment. For flexibility—and because it is needed
by actual theories of interest—the theory solver should be able to demand case
splits on literals that may be unfamiliar to the DPLL engine and may possibly
even contain fresh constant symbols. Here, we give a brief explanation of how this
can be done in the context of the abstract framework given in §12.4.4. Details
can be found in [BNOT06a].
770 Chapter 12. Satisfiability Modulo Theories
Recall that in the abstract framework, the T -Learn rule allows the theory
solver to add an arbitrary clause to those being processed by the DPLL engine,
so long as all the atoms in that clause are already known to the DPLL engine. Our
approach will be to relax this restriction. It is not hard to see, however, that this
poses a potential termination problem. We can overcome this difficulty so long as
for any input formula φ, the set of all literals needed to check the T -consistency
of φ is finite. We formalize this notion by introducing the following definition.
Definition 12.5.6. L is a suitable literal-generating function if for every finite
set of literals L:
1. L maps L to a new finite set of literals L′ such that L ⊆ L′ .
2. For each atomic formula α, α ∈ L(L) iff ¬α ∈ L(L).
3. If L′ is a set of literals and L ⊆ L′ , then, L(L) ⊆ L(L′ ) (monotonicity).
4. L(L(L)) = L(L) (idempotence).
For convenience, given a formula φ, we denote by L(φ) the result of applying L to
the set of all literals appearing in φ. In order to be able to safely use splitting on
demand for a theory solver T -solver, we must be able to show the existence of a
suitable literal-generating function L such that: for every input formula φ, the set
of all literals on which the T -solver may demand case splits when starting with
a conjunction of literals from φ is contained in L(φ). For example, for T A , L(φ)
could contain atoms of the form i = j, where i and j are array indices occurring
in φ. Note that there is no need to explicitly construct L(φ). It is enough to
know that it exists.
As mentioned above, it is sometimes useful to demand case splits on literals
containing new constant symbols. The introduction of new constant symbols
poses potential problems not only for termination, but also for soundness. This
is because the abstract framework relies on the fact that whenever ∅ || φ reduces
in one or more steps to µ || φ′ , the formulas φ and φ′ are T -equivalent. This is
no longer true if we allow the introduction of new constant symbols. Fortunately,
it is sufficient to ensure T -equisatisfiability of φ and φ′ . With this in mind, we
can give a new transition rule called Extended T-Learn which replaces T -Learn and
allows for the desired additional flexibility.
Definition 12.5.7. The Extended DPLL Modulo Theories system, consists of the
rules of §12.4.4 except that the T -Learn rule is replaced by the following24 rule:
Extended T-Learn
each atom of c occurs in φ or in L(µ)
µ || φ =⇒ µ || φ, c if
φ |=T γφ (c)
The key observation is that an implementation using Extended T-Learn has more
flexibility when a state µ || φ is reached that is final with respect to the basic rules
Propagate, Decide, Fail, and T -Backjump. Whereas before it would have been nec-
essary to determine the T -consistency of µ when such a state was reached, the
Extended T-Learn rule allows the possibility of delaying a response by demanding
that additional case splits be done first. As shown in [BNOT06a], the extended
24 The definition of γ was given in §12.5.1.
Chapter 12. Satisfiability Modulo Theories 771
Sometimes, a theory T has the property that a fully general solver for T is not
always needed: rather, the unsatisfiability of an assignment µ can often be es-
tablished in less expressive, but much easier, sub-theories. Thus, the T -solver
may be organized in a layered hierarchy of solvers of increasing solving capabili-
ties [ABC+ 02, BBC+ 05a, SS05, CM06b, BCF+ 07]. The general idea consists of
stratifying the problem over N layers L0 , L1 , . . . , LN −1 of increasing complexity,
and searching for a solution “at as simple a level as possible”. If one of the sim-
pler solvers finds a conflict, then this conflict is used to prune the search at the
Boolean level; if it does not, the next solver in the sequence is activated.
Since Ln+1 refines Ln , if the set of literals is not satisfiable at level Ln , then it
is not at Ln+1 , . . . , LN −1 . If indeed a model S exists at Ln , either n equals N − 1,
772 Chapter 12. Satisfiability Modulo Theories
Another approach for building theory solvers relies on the power and flexibility of
modern automated theorem provers, in particular, provers based on the superpo-
sition calculus [NR01], a modern version of the resolution calculus for first-order
logic with equality. This calculus is based on term rewriting techniques and comes
equipped with powerful redundancy criteria that allow one to build very effective
control strategies for reducing the search space.
The superposition-based approach to SMT, first proposed in [ARR03] and
then further elaborated upon in [ABRS05, BGN+ 06a, BE07a, BE07b], applies to
theories T that are axiomatizable by a finite (and relatively small) set of first-
order clauses, such as for instance the theory of arrays in §12.2.2. The main
idea is to instrument a superposition prover with specialized control strategies
which, together with the axioms of T , effectively turn the prover into a decision
procedure for ground T -satisfiability.
An advantage of the approach is a simplified proof of correctness, even in the
case of combined theories, which reduces to a routine proof of termination of the
application of the various superposition rules (see, e.g., [ARR03] for details). An-
other potential advantage is the reuse of efficient data structures and algorithms
for automated deduction implemented in state-of-the-art theorem provers. The
main disadvantage is that to get additional features typically required in SMT
such as model generation, incrementality, and so on, one may need to modify
the theorem prover in ways not foreseen by the original implementors, possibly
at the cost of a considerable (re)implementation effort. While this approach has
generated an active stream of interesting theoretical work, its practical impact
has been limited so far by a scarcity of robust and competitive implementations.
We mentioned that in SMT one is often faced with formulas involving several
theories at once. This is particularly true in software verification, where proof
obligations are formulas talking about several datatypes, each modeled by its
own theory. We have seen that for many of these theories the ground satisfiabil-
ity problem is decidable, and often by efficient theory solvers. Hence, a natural
question is whether it is possible to combine theory solvers for several component
theories T 1 , . . . , T n modularly into a theory solver that decides ground satisfia-
bility modulo their combination T 1 ⊕ · · · ⊕ T n .
Chapter 12. Satisfiability Modulo Theories 773
In general, the answer is negative, simply because there exist theories with
a decidable ground satisfiability problem whose combination has an undecidable
ground satisfiability problem (see, e.g., [BGN+ 06b]). Positive results are however
possible by imposing restrictions on the component theories and their combi-
nation. A successful combination method for theory solvers is due to Nelson
and Oppen [NO79]. The success of the method is based on the fact that its
restrictions on the theories are not very strong in practice, and lead to effi-
cient implementations. It is fair to say that most work in theory combination
in SMT is based on extensions and refinements of Nelson and Oppen’s work
(see, e.g., [TH96, Rin96, BDS02c, TR03, TZ04, Ghi04, TZ05, RRZ05, GNZ05,
BBC+ 06, GNRZ06, CK06, BNOT06a, KGGT07]).
In this section, we present a declarative non-deterministic combination frame-
work, first presented in [Opp80b], that captures the essence of the original com-
bination procedure by Nelson and Oppen in [NO79], and briefly discuss a few
variants and extensions. Then we describe how an efficient implementation of
this framework can be incorporated into the lazy approach to SMT.
For simplicity, we consider just the case of combining two theories and their
solvers since the case of more theories is analogous. Therefore, let Σ1 , Σ2 be two
signatures and let T i be a Σi theory for i = 1, 2. The combination of T 1 and T2
will be the theory T 1 ⊕ T 2 as defined in §12.2.1.3.
It is not hard to see that this procedure always terminates, runs in time linear
in the size of ϕ, and produces a formula ϕ1 ∧ ϕ2 that is equisatisfiable with ϕ.
More precisely, every model of ϕ1 ∧ϕ2 is also a model of ϕ, and for every model A
of ϕ there is a model of ϕ1 ∧ ϕ2 that differs from A at most in the interpretation
of the new constants introduced in the abstraction step above.
The constraint propagation mechanism of the original Nelson-Oppen pro-
cedure can be abstracted by a preliminary non-deterministic guess of a truth
assignment for all possible interface equalities, that is, equations between the
(uninterpreted) constants shared by ϕ1 and ϕ2 . To describe that, it is convenient
to introduce the following notion [TH96].
Let R be any equivalence relation over a finite set S of terms. The arrange-
ment of S induced by R is the formula
^ ^
arR (S) := (s = t) ∧ s 6= t
(s,t)∈R (s,t)∈R
/
containing all equations between R-equivalent terms and all disequations between
non-R-equivalent terms of S.
The combination procedure below just guesses an arrangement of the shared
constants in a pure form ϕ1 ∧ ϕ2 of ϕ, adds it to each ϕi , and then asks the
corresponding theory solver to check the satifiability of the extended ϕi .
25 Note that (dis)equations between constants of C end up in both ϕ1 and ϕ2 .
Chapter 12. Satisfiability Modulo Theories 775
The first (correct) proof of the result above was given in [Opp80b]. More
recent proofs based on model-theoretic arguments can be found in [TH96, MZ03b,
Ghi04], among others.27 The completeness result in the original paper by Nelson
and Oppen [NO79] is incorrect as stated because it imposes no restrictions on
the component theories other than that they should be signature-disjoint. The
completeness proof however is incorrect only because it implicitly assumes there
is no loss of generality in considering only infinite models, which is however not
the case unless the theories are stably infinite.
We remark that the stable infiniteness requirement is not an artifice of a par-
ticular completeness proof. The combination method is really incomplete without
it, as shown for instance in [TZ05]. This is a concern because non-stably infinite
theories of practical relevance do exist. For instance, all the theories of a single
finite model, such as the theory of bit-vectors (or of strings) with some maximum
size, are not stably infinite.
Current practice and recent theoretical work have shown that it is possible
to lift the stable infiniteness requirement in a number of ways provided that the
combination method is modified to include the propagation of certain cardinality
26 Observe that there is always a finite, albeit possibly very large, set of arrangements for any
stating that l1 , l2 , l3 are distinct lists of length 1, entails the existence of at least
3 distinct values for the element type Bool. If ϕ1 above is part of the formula
sent to the list solver, its entailed minimal cardinality constraint on the Bool
type must be communicated to the theory solver for that type. Otherwise, the
unsatisfiability of ϕ1 in the combined theory of List(Bool) will go undetected. A
description of how it is possible to propagate cardinality constraints conveniently
for theories of typical parametric datatypes, such as lists, tuples, arrays and so on,
can be found in [RRZ05]. A discussion on why in a typed setting parametricity
and not stable infiniteness is the key notion to consider for Nelson-Oppen style
combination is provided in [KGGT07].
procedure—including its authors—it was (and still is) often overlooked by casual readers.
Chapter 12. Satisfiability Modulo Theories 777
has any new equalities to propagate. In the latter case, it is safe to conclude that
the input formula is satisfiable in the combined theory.
When one of the two theories, or both, are non-convex, exchanging just en-
tailed interface equalities is no longer enough for completeness. The solver for the
non-convex theory must be able to infer, and must propagate, also any disjunction
of interface equality entailed by its pure half of the formula. Correspondingly, the
other solver must be able to process such disjunctions, perhaps by case splits, in
addition to the conjunction of literals in the original input.
For convex theories—such as, for instance T E —computing the interface equal-
ities entailed by a conjunction ϕ of literals can be done very efficiently, typically
as a by-product of checking ϕ’s satisfiability (see, e.g., [NO03, NO05b]). For non-
convex theories, on the other hand, computing entailed disjunctions of equalities
can be rather expensive both in practice and in theory. For instance, for the dif-
ference logic fragment of T Z , this entailment problem is NP-complete even if the
satisfiability of conjunctions of literals can be decided in polynomial time [LM05].
Delayed Theory Combination( Dtc) is a general method for tackling the problem
of theory combination within the context of lazy SMT [BBC+ 05c, BBC+ 06]. As
in §12.6.1, we assume that T1 , T2 are two signature-disjoint stably-infinite theories
with their respective Ti -solvers. Importantly, no assumption is made about the
capability of the Ti -solvers of deducing (disjunctions of) interface equalities from
the input set of literals (eij -deduction capabilities, see §12.4.1): for each Ti -solver,
every intermediate situation from complete eij -deduction (like in deterministic
Nelson-Oppen) to no eij -deduction capabilities (like in non-deterministic Nelson-
Oppen) is admitted.
In a nutshell, in Dtc the embedded DPLL engine not only enumerates truth-
assignments for the atoms of the input formula, but also “nondeterministically
guesses” truth values for the equalities that the T -solvers are not capable of
inferring, and handles the case-split induced by the entailment of disjunctions of
interface equalities in non-convex theories. The rationale is to exploit the full
power of a modern DPLL engine by delegating to it part of the heavy reasoning
effort previously assigned to the Ti -solvers.
An implementation of Dtc [BBC+ 06, BCF+ 06b] is based on the online in-
tegration schema of Figure 12.3, exploiting early pruning, T -propagation, T -
backjumping and T -learning. Each of the two Ti -solvers interacts only with the
DPLL engine by exchanging literals via the truth assignment µ in a stack-based
manner, so that there is no direct exchange of information between the Ti -solvers.
Let T be T1 ∪ T2 . The T -DPLL algorithm is modified in the following ways
[BBC+ 06, BCF+ 06b]:29
• T -DPLL must be instructed to assign truth values not only to the atoms in
ϕ, but also to the interface equalities not occurring in ϕ. B2T and T 2B are
modified accordingly. In particular, T -decide next branch is modified to
select also new interface equalities not occurring in the original formula.
29 For simplicity, we assume ϕ is pure, although this condition is not necessary, as in [BDS02b].
778 Chapter 12. Satisfiability Modulo Theories
µE : µZ :
¬(f (v1) = f (v2)) v1 ≥ 0 v5 = v4 − 1
¬(f (v2) = f (v4)) v1 ≤ 1 v3 = 0
f (v3) = v5 v2 ≥ v6 v4 = 1
f (v1) = v6 v2 ≤ v6 + 1
v1 = v4
¬(v1 = v4)
v1 = v3
¬(v1 = v3) v5 = v6
T Z -unsat, C13 v2 = v4
¬(v5 = v6) T E -unsat, C14
T E -unsat, C56 C13 : (µ′Z ) → ((v1 = v3) ∨ (v1 = v4))
¬(v2 = v4) C56 : (µ′E ∧ (v1 = v3)) → (v5 = v6)
v2 = v3 C23 : (µ′′Z ∧ (v5 = v6)) → ((v2 = v3) ∨ (v2 = v4))
¬(v2 = v3) T E -unsat, C24
C24 : (µ′′E ∧ (v1 = v3) ∧ (v2 = v3)) → ⊥
T Z -unsat, C23 C14 : (µ′′′
E ∧ (v1 = v3) ∧ (v2 = v4)) → ⊥
Figure 12.6. The Dtc search tree for Example 12.6.3 on T Z ∪ T E , with no eij -deduction.
v1 , . . . , v6 are interface terms. µ′T , µ′′ ′′′
T , µT denote appropriate subsets of µT i , Ti ∈ {T E , T Z }.
i i i
• µp is partitioned into three components µpT1 , µpT2 and µpe , s.t. µTi is the set
of i-pure literals and µe is the set of interface (dis)equalities in µ.
• T -deduce is modified to work as follows: for each Ti , µpT i ∪ µpe , is fed to
the respective Ti -solver. If both return Sat, then T -deduce returns Sat,
otherwise it returns Conflict.
• Early-pruning is performed; if some Ti -solver can deduce atoms or single
interface equalities, then T -propagation
W is performed. If one Ti -solver per-
forms the deduction µ∗ |=Ti kj=1 ej , s.t. µ∗ ⊆ µT i ∪ µe , each ej being an
Wk
interface equality, then the deduction clause T 2B(µ∗ → j=1 ej ) is learned.
• T -analyze conflict and T -backtrack are modified so as to use the con-
flict set returned by one Ti -solver for T -backjumping and T -learning. Im-
portantly, such conflict sets may contain interface equalities.
In order to achieve efficiency, other heuristics and strategies have been further
suggested in [BBC+ 05c, BBC+ 06, BCF+ 06b, DdM06a, dMB07].
Example 12.6.3. [BCF+ 06b] Consider the set of T E ∪T Z -literals µ =def µE ∧µZ
of Figure 12.6. We assume that both the T E and T Z solvers have no eij -deduction
capabilities. For simplicity, we also assume that both Ti -solvers always return
conflict sets which do not contain redundant interface disequalities ¬eij . (We
adopt here a strategy for Dtc which is described in detail in [BCF+ 06b].) In
short, T -DPLL performs a Boolean search on the eij ’s, backjumping on the
conflicting clauses C13 , C56 , C23 , C24 and C14 , which in the end causes the unit-
propagation of (v1 = v4 ). Then, T -DPLL selects a sequence of ¬eij ’s without
generating conflicts, and concludes that the formula is T1 ∪ T2 -satisfiable. Notice
Chapter 12. Satisfiability Modulo Theories 779
that the backjumping steps on the clauses C13 , C56 , and C23 mimic the effects of
performing eij -deductions.
By adopting T -solvers with different eij -deduction power, one can trade part
or all the eij -deduction effort for extra Boolean search. [BCF+ 06b] shows that, if
the T -solvers have full eij -deduction capabilities, then no extra Boolean search on
the eij ’s is required; otherwise, the Boolean search is controlled by the quality of
the conflict sets returned by the T -solvers: the more redundant interface disequal-
ities are removed from the conflict sets, the more Boolean branches are pruned. If
the conflict sets do not contain redundant interface disequalities, the extra effort
is reduced to one branch for each deduction saved, as in Example 12.6.3.
As seen in §12.5.2, the idea from Dtc of delegating to the DPLL engine part
or most of the, possibly very expensive, reasoning effort normally assigned to the
Ti -solvers (eij -deduction, case-splits) is pushed even further in the splitting on
demand approach. As far as multiple theories are concerned, the latter approach
differs from Dtc in the fact that the interaction is controlled by the Ti -solvers,
not by the DPLL engine. Other improvements of Dtc are currently implemented
in the MathSAT [BBC+ 06], Yices [DdM06a], and Z3 [dMB07] lazy SMT tools.
In particular, [DdM06a] introduced the idea of generating eij ’s on-demand, and
[dMB07] that of having the Boolean search on eij ’s driven by a model under
construction.
When combining one or more theories with T E , one possible approach is to elimi-
nate uninterpreted function symbols by means of Ackermann’s expansion [Ack54].
The method works as described in §12.3.1.3 by replacing every function applica-
tion occurring in the input formula ϕ with a fresh variable and then adding to ϕ
all the needed functional congruence constraints. The formula ϕ′ obtained is eq-
uisatisfiable with ϕ, and contains no uninterpreted function symbols. [BCF+ 06a]
presents a comparison between Dtc and Ackermann’s expansion.
µE : ¬(vf (v1 ) = vf (v2 ) ) ∧ ¬(vf (v2 ) = vf (v4 ) ) ∧ (vf (v3 ) = v5 ) ∧ (vf (v1 ) = v6 )∧
µZ : (v1 ≥ 0) ∧ (v1 ≤ 1) ∧ (v5 = v4 − 1) ∧ (v3 = 0) ∧ (v4 = 1)∧
(v2 ≥ v6 ) ∧ (v2 ≤ v6 + 1)∧
Ack : ((v1 = v2 ) → (vf (v1 ) = vf (v2 ) )) ∧ ((v1 = v3 ) → (vf (v1 ) = vf (v3 ) ))∧
((v1 = v4 ) → (vf (v1 ) = vf (v4 ) )) ∧ ((v2 = v3 ) → (vf (v2 ) = vf (v3 ) ))∧
((v2 = v4 ) → (vf (v2 ) = vf (v4 ) )) ∧ ((v3 = v4 ) → (vf (v3 ) = vf (v4 ) )),
(12.2)
which every T Z -solver finds T Z -satisfiable. (E.g., the T Z -model v2 = 2, v3 =
v5 = v6 = vf (v1 ) = vf (v3 ) = 0, v1 = v4 = vf (v2 ) = vf (v4 ) = 1 satisfies it.)
780 Chapter 12. Satisfiability Modulo Theories
The Ackermann expansion described above is one way to combine eager and
lazy approaches. Other hybrids of eager and lazy encoding methods can also be
effective.
For instance, consider the satisfiability problem for integer linear arithmetic
and the small-domain encoding technique presented in §12.3.2. Due to the con-
servative nature of the bound derived, and in spite of the many optimizations
possible, the computed solution bound can generate a SAT problem beyond the
reach of current solvers. For example, this situation can arise for problem domains
that do not generate sparse linear constraints.
One can observe that the derived bounds are dependent only on the “bag
of constraints”, rather than on their specific Boolean combination in the input
formula. Thus, there is hope that a smaller solution bound might suffice. Kroen-
ing et al. [KOSS04] have presented an approach to compute the solution bound
incrementally, starting with a small bound and increasing it “on demand”. Fig-
ure 12.7 outlines this lazy approach to computing the solution bound. Given a
Select small
solution bound
d
YES
Proof
Boolean Generate Is
Formula Sound Abstraction
Satisfiable? NO Satisfiable?
Abstraction
YES NO
T Z -formula FZ , we start with an encoding size for each integer variable that is
smaller than that prescribed by the conservative bound (say, for example, 1 bit
per variable).
Chapter 12. Satisfiability Modulo Theories 781
Because the Nelson-Oppen framework (§12.6.1) only works for quantifier-free for-
mulas, SMT solvers have traditionally been rather limited in their ability to reason
about quantifiers. A notable exception is the prover Simplify [DNS03] which uses
quantifier instantiation on top of a Nelson-Oppen style prover. Several mod-
ern SMT solvers have adopted and extended these techniques [GBT07, BdM07,
ML06].
The basic idea can be understood by extending the abstract framework de-
scribed in §12.4.4 to include rules for quantifier instantiation. The main modi-
fication is to also allow closed quantified formulas wherever atomic formulas are
allowed. Define a generalized atomic formula as either an atomic formula or a
closed quantified formula. A generalized literal is either a generalized atomic
formula or its negation; a generalized clause is a disjunction of generalized liter-
als. The modified abstract framework is obtained simply by allowing literals and
clauses to be replaced by their generalized counterparts. For instance, non-fail
states become pairs M || F , where M is a sequence of generalized literals and
F is a conjunction of generalized clauses. With this understanding, the two rules
below can be used to model quantifier instantiation. For simplicity and without
782 Chapter 12. Satisfiability Modulo Theories
loss of generality, we assume here that quantified literals in M appear only posi-
tively and that the bodies of quantified formulas are themselves in abstract CNF.
∃x.ϕ is in M
∃-Inst : M || F =⇒ M || F, ¬∃x.ϕ ∨ ϕ[x/a] if
a are fresh constants
∀x.ϕ is in M
∀-Inst : M || F =⇒ M || F, ¬∀x.ϕ ∨ ϕ[x/s] if
s are ground terms
The ∃-Inst rule essentially models skolemization and the ∀-Inst rule models in-
stantiation. It is also clear that termination can only be guaranteed by limiting
the number of times the rules are applied. For a given existentially quantified
formula, there is no benefit to applying ∃-Inst more than once, but a universally
quantified formula may need to be instantiated several times with different ground
terms before unsatisfiability is detected. The main challenge then, in applying
these rules, is to come up with an effective strategy for applying ∀-Inst. For some
background theories (e.g., universal theories) completeness can be shown for ex-
haustive and fair instantiation strategies. In practice, however, the most effective
techniques are incomplete and heuristic.
The most common approach is to select for instantiation only ground terms
that are relevant to the quantified formula in question, according to some heuristic
relevance criteria. The idea is as follows: given a state M || F and an abstract
literal ∀ x.ϕ in M , try to find a subterm t of ∀x.ϕ properly containing x, a ground
term g in M , and a subterm s of g, such that t[x/s] is equivalent to g modulo
the background theory T (written t[x/s] =T g). In this case, we expect that
instantiating x with s is more likely to be helpful than instantiating with other
candidate terms. Following Simplify’s terminology, the term t is called a trigger
(for ∀x.ϕ). In terms of unification theory, the case in which t[x/s] =T g is a
special case of T -matching between t and g.
In general, in the context of SMT, given the complexity of the background
theory T , it may be very difficult if not impossible to determine whether a trigger
and a ground term T -match. As a result, most implementations use some form
of T E -matching. For details on effective implementation strategies, we refer the
reader to [DNS03, GBT07, BdM07, ML06].
In both SAT and SMT communities, the importance of having tools able to
produce proofs of the (T -)unsatisfiability of the input formulas has been recently
stressed, due to the need for independently verifiable results, and as a starting
point for the production of unsatisfiable cores (§12.7.5) and interpolants (§12.7.6).
A DPLL solver can be easily modified to generate a resolution proof of un-
satisfiability for an input CNF formula, by keeping track of all resolution steps
performed when generating each conflict clause, and by combining these subproofs
iteratively into a proof of unsatisfiability whose leaves are original clauses. Tech-
niques for translating a Boolean resolution proof into a more human-readable and
verifiable format have been proposed, e.g., in [BB03, Amj07].
Similarly, a lazy SMT solver can be modified to generate a resolution proof of
unsatisfiability for an input CNF formula, whose leaves are either clauses from the
original formula or T -lemmas (i.e. negations of T -conflict sets and T -deduction
clauses returned by the T -solver, see §12.4.3), which are T -valid clauses. Such a
resolution proof can be further refined by providing a proof for each T -lemma in
some theory-specific deductive framework (like, e.g. that in [McM05] for inequal-
ities in T R ).
cores in these tools comes from personal knowledge of the tools (CVC3 and MathSAT) and
from private communications from the authors (Yices).
784 Chapter 12. Satisfiability Modulo Theories
References
1996.
[HMNT93] Dorit Hochbaum, N. Megiddo, J. Naor, and A. Tamir. Tight bounds
and 2-approximation algorithms for integer programs with two vari-
ables per inequality. Mathematical Programming, 62:63–92, 1993.
[Hor98] I. Horrocks. The FaCT system. In H. de Swart, editor, Proc.
TABLEAUX-98, volume 1397 of LNAI, pages 307–312. Springer,
1998.
[Hua05] J. Huang. MUP: a minimal unsatisfiability prover. In Proc. ASP-
DAC ’05. ACM Press, 2005.
[JMSY94] Joxan Jaffar, Michael J. Maher, Peter J. Stuckey, and Roland H. C.
Yap. Beyond finite domains. In 2nd International Workshop on Prin-
ciples and Practice of Constraint Programming (PPCP’94), volume
874 of Lecture Notes in Computer Science, pages 86–94, 1994.
[Kar84] N. Karmakar. A new polynomial-time algorithm for linear program-
ming. Combinatorica, 4(4):373–395, 1984.
[KC03] Sava Krstić and Sylvain Conchon. Canonization for disjoint unions
of theories. In Franz Baader, editor, Proceedings of the 19th Interna-
tional Conference on Computer-Aided Deduction (CADE ’03), vol-
ume 2741 of Lecture Notes in Artificial Intelligence, pages 197–211.
Springer, August 2003. Miami Beach, FL.
[KGGT07] Sava Krstić, Amit Goel, Jim Grundy, and Cesare Tinelli. Com-
bined satisfiability modulo parametric theories. In O. Grumberg and
M. Huth, editors, Proceedings of the 13th International Conference
on Tools and Algorithms for the Construction and Analysis of Sys-
tems (Braga, Portugal), volume 4424 of Lecture Notes in Computer
Science, pages 618–631. Springer, 2007.
[KM78] R. Kannan and C. L. Monma. On the computational complexity of
integer programming problems. In Optimisation and Operations Re-
search, volume 157 of Lecture Notes in Economics and Mathematical
Systems, pages 161–172. Springer-Verlag, 1978.
[KMZ06] Deepak Kapur, Rupak Majumdar, and Calogero G. Zarba. Interpo-
lation for data structures. In Proc. SIGSOFT FSE. ACM, 2006.
[KOSS04] Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, and Ofer Strich-
man. Abstraction-based satisfiability solving of Presburger arith-
metic. In Proc. 16th International Conference on Computer-Aided
Verification (CAV), pages 308–320, July 2004.
[KW07] Daniel Kroening and Georg Weissenbacher. Lifting propositional
interpolants to the word-level. In Proceedings of FMCAD, pages 85–
89. IEEE, 2007.
[LB03] Shuvendu K. Lahiri and Randal E. Bryant. Deductive verification of
advanced out-of-order microprocessors. In Proc. 15th International
Conference on Computer-Aided Verification (CAV), volume 2725 of
LNCS, pages 341–354, 2003.
[LBGT04] Shuvendu K. Lahiri, Randal E. Bryant, Amit Goel, and Muralidhar
Talupur. Revisiting positive equality. In Proc. Tools and Algoriths
for the Construction and Analysis of Systems (TACAS), LNCS 2988,
pages 1–15, 2004.
Chapter 12. Satisfiability Modulo Theories 793
July 1980.
[Opp80b] Derek C. Oppen. Complexity, convexity and combinations of theo-
ries. Theoretical Computer Science, 12:291–302, 1980.
[Pap81] C. H. Papadimitriou. On the complexity of integer programming.
Journal of the Association for Computing Machinery, 28(4):765–768,
1981.
[Pra77] Vaughan Pratt. Two easy theories whose combination is hard. Tech-
nical report, Massachusetts Institute of Technology, 1977. Cam-
bridge, MA.
[PRSS99] A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equal-
ity formulas by small domains instantiations. In Proceedings of the
11th International Conference on Computer Aided Verification, vol-
ume 1633 of Lecture Notes in Computer Science, pages 455–469.
Springer, 1999.
[PRSS02] A. Pnueli, Y. Rodeh, M. Siegel, and O. Strichman. The small model
property: How small can it be? Journal of Information and Com-
putation, 178(1):279–293, October 2002.
[PS98] P. F. Patel-Schneider. DLP system description. In Proc. DL-98,
pages 87–89, 1998.
[Pud97] Pavel Pudlák. Lower bounds for resolution and cutting planes proofs
and monotone computations. J. of Symbolic Logic, 62(3), 1997.
[Pug91] William Pugh. The omega test: A fast and practical integer pro-
gramming algorithm for dependence analysis. In Supercomputing,
pages 4–13, 1991.
[Rin96] Christophe Ringeissen. Cooperation of decision procedures for the
satisfiability problem. In F. Baader and K.U. Schulz, editors,
Frontiers of Combining Systems: Proceedings of the 1st Interna-
tional Workshop, Munich (Germany), Applied Logic, pages 121–140.
Kluwer Academic Publishers, March 1996.
[RRZ05] Silvio Ranise, Christophe Ringeissen, and Calogero G. Zarba. Com-
bining data structures with nonstably infinite theories using many-
sorted logic. In B. Gramlich, editor, Proceedings of the Workshop
on Frontiers of Combining Systems, volume 3717 of Lecture Notes in
Computer Science, pages 48–64. Springer, 2005.
[RS01] Harald. Ruess and Natarajan Shankar. Deconstructing Shostak. In
16th Annual IEEE Symposium on Logic in Computer Science, pages
19–28. IEEE Computer Society, June 2001. Boston, MA.
[RSS07] Andrey Rybalchenko and Viorica Sofronie-Stokkermans. Constraint
Solving for Interpolation. In VMCAI, LNCS. Springer, 2007.
[SB05] Sanjit A. Seshia and Randal E. Bryant. Deciding quantifier-free
Presburger formulas using parameterized solution bounds. Logical
Methods in Computer Science, 1(2):1–26, December 2005.
[SBD02] Aaron Stump, Clark W. Barrett, and David L. Dill. CVC: A cooper-
ating validity checker. In Ed Brinksma and Kim Guldstrand Larsen,
editors, Proceedings of the 14th International Conference on Com-
puter Aided Verification (CAV ’02), volume 2404 of Lecture Notes in
Computer Science, pages 500–504. Springer, July 2002.
796 Chapter 12. Satisfiability Modulo Theories
[SDBL01] Aaron Stump, David L. Dill, Clark W. Barrett, and Jeremy Levitt. A
decision procedure for an extensional theory of arrays. In Proceedings
of the 16th IEEE Symposium on Logic in Computer Science (LICS
’01), pages 29–37. IEEE Computer Society, June 2001.
[Seb07] R. Sebastiani. Lazy Satisfiability Modulo Theories. Journal on Sat-
isfiability, Boolean Modeling and Computation – JSAT., 3, 2007.
[Ses05] Sanjit A. Seshia. Adaptive Eager Boolean Encoding for Arithmetic
Reasoning in Verification. PhD thesis, Carnegie Mellon University,
2005.
[Sho78] Robert E. Shostak. An algorithm for reasoning about equality. Com-
munications of the ACM, 21(7), 1978.
[Sho79] Robert E. Shostak. A practical decision procedure for arithmetic
with function symbols. Journal of the ACM, 26(2):351–360, April
1979.
[Sho84] R. Shostak. Deciding combinations of theories. Journal of the Asso-
ciation for Computing Machinery, 31(1):1–12, 1984.
[SJ80] Norihisa Suzuki and David Jefferson. Verification decidability of
presburger array programs. J. ACM, 27(1):191–205, 1980.
[SLB03] S. A. Seshia, S. K. Lahiri, and R. E. Bryant. A hybrid SAT-based
decision procedure for separation logic with uninterpreted functions.
In 40th Design Automation Conference (DAC ’03), pages 425–430,
June 2003.
[SR02] Natarajan Shankar and Harald Rueß. Combining Shostak theories.
In Sophie Tison, editor, Int’l Conf. Rewriting Techniques and Ap-
plications (RTA ’02), volume 2378 of LNCS, pages 1–18. Springer,
2002.
[SS05] Hossein M. Sheini and Karem A. Sakallah. A scalable method for
solving satisfiability of integer linear arithmetic logic. In Fahiem Bac-
chus and Toby Walsh, editors, Proceedings of the 8th International
Conference on Theory and Applications of Satisfiability Testing (SAT
’05), volume 3569 of Lecture Notes in Computer Science, pages 241–
256. Springer, June 2005.
[SS06] H. M. Sheini and K. A. Sakallah. A Progressive Simplifier for Satis-
fiability Modulo Theories. In Proc. SAT’06, volume 4121 of LNCS.
Springer, 2006.
[SSB02] O. Strichman, S. A. Seshia, and R. E. Bryant. Deciding separa-
tion formulas with SAT. In E. Brinksma and K. G. Larsen, ed-
itors, Proc. 14th Intl. Conference on Computer-Aided Verification
(CAV’02), LNCS 2404, pages 209–222. Springer-Verlag, July 2002.
[SSB07] S. A. Seshia, K. Subramani, and R. E. Bryant. On solving
boolean combinations of UTVPI constraints. Journal of Satisfia-
bility, Boolean Modeling, and Computation (JSAT), 3:67–90, 2007.
[Str02a] O. Strichman. On solving Presburger and linear arithmetic with
SAT. In Formal Methods in Computer-Aided Design (FMCAD ’02),
LNCS 2517, pages 160–170. Springer-Verlag, November 2002.
[Str02b] O. Strichman. Optimizations in decision procedures for propositional
linear inequalities. Technical Report CMU-CS-02-133, Carnegie Mel-
Chapter 12. Satisfiability Modulo Theories 797