SMT 2007

Model-based Theory Combination

Leonardo de Moura1 Nikolaj Bjørner2

Microsoft Research, One Microsoft Way, Redmond, WA, 98074, USA

Abstract
Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied
equalities or a pre-processing step that introduces additional literals into the search space. This paper
introduces a combination method that incrementally reconciles models maintained by each theory. We
evaluate the practicality and efficiency of this approach.

Keywords: Theory Combination, Decision Procedures, SMT solvers.

1 Introduction
A core problem of Satisfiability Modulo Theories is combining separate theory
solvers for theories T 1 and T 2 to a combined solver for the union T 1 ∪ T 2 . The
Nelson-Oppen combination method identifies sufficient conditions for combining two
theories over disjoint signatures: only (disjunctions of) equalities over shared vari-
ables that are implied by one of the theories need to be communicated. Most existing
implementations and optimizations of this method seek to efficiently implement the
trigger:
if T i ∪ Γi |= u ' v then propagate u ' v,
to exhaustively enumerating all implied (disjunctions of) equalities for a theory T i
and constraints Γi that are asserted in its context. Another method [1] to obtain
completeness is by enumerating equalities corresponding to the cross-product of all
shared variable pairs and use the SAT solver for non-deterministically choosing a
partition based on the cross-product. Common to these methods is that they are
pessimistic about which equalities are propagated. A more optimistic approach is
by inspecting a candidate model Mi for one of the theories T i and propagate all
equalities implied by the candidate model, hedging that other theories will agree.

1 Email: leonardo@microsoft.comu
2 Email: nbjorner@microsoft.com
This paper is electronically published in
Electronic Notes in Theoretical Computer Science
URL: www.elsevier.nl/locate/entcs
 de Moura, Bjørner

If not, use backtracking to fix the model. Thus, Model-based Theory Combination
is based on a trigger of the form:
if Mi |= T i ∪ Γi ∪ {u ' v} then propagate u ' v .
The rationale for Model-based Theory Combination is practical: It tends to be
much cheaper to enumerate equalities that are implied in a particular model than
of all models; the number of inter-theory equalities that really matter is small in
practice (intra-theory equality propagation on the other hand does matter); back-
tracking is relatively cheap with modern DPLL solvers; and finally, one may limit
the number of equalities implied by a model by model mutation.

2 Background
A signature Σ is a set of function and predicate symbols. Each symbol is associated
with a nonnegative integer, called the arity. If arity(g) = 0, then g is a constant
symbol. We assume that the binary equality predicate ' to be always present in
any signature Σ. We use the standard notion of Σ-structure M, that is, a support
set endowed with an arity-matching interpretation of the function and predicate
symbols from Σ. We use f M (pM ) to denote the interpretation of the function
symbol f (predicate symbol p) in the structure M. The truth of a Σ-formula in M
is defined in the standard ways. A formula φ is satisfiable in M iff its existential
closure is true in M. In this case, we say M is a model for φ. A sentence is a
first-order formula with no free variables. A (first-order) theory T over a signature
Σ is a set of (deductively closed) sentences over Σ. We say two theories T 1 and
T 2 have disjoint signatures when Σ1 ∩ Σ2 = {'}. A theory T is stably infinite
if every satisfiable quantifier free formula is satisfiable in an infinite model. A
theory T is convex [2] iff for all finite sets Γ of literals and for all non-empty
W W
disjunctions i∈I ui ' vi of variables, Γ |=T i∈I ui ' vi iff Γ |=T ui ' vi for some
i ∈ I. Intuitively, a theory is convex if for every satisfiable set of literals there
is a model where variables not implied to be equal have a distinct interpretation.
For example, linear integer arithmetic is not convex, because the set of literals
{0 ≤ x1 ≤ 1, 0 ≤ x2 ≤ 1, 0 ≤ x3 ≤ 1} is satisfiable, no equality xi ' xj for i 6= j is
implied, but there is no model where x1 , x2 and x3 are all distinct.

2.1 Nelson-Oppen combination method

Nelson-Oppen (NO) combination method [3] provides a rather simple solution for
the theory combination problem for theories that are stably infinite and have disjoint
theories. More formally, let T 1 and T 2 be consistent, stably infinite theories over
disjoint (countable) signatures. Assuming satisfiability of conjunction of literals can
be decided in O(T 1 (n)) and O(T 2 (n)) time respectively. Then,
(i) The combined theory T is consistent and stably infinite.
(ii) Satisfiability of quantifier free conjunction of literals in T can be decided in
2
O(2n × (T 1 (n) + T 2 (n))).
(iii) If T 1 and T 2 are convex, then so is T and satisfiability in T is in O(n4 ×
(T 1 (n) + T 2 (n))).
2
 de Moura, Bjørner

Let Γ be a set of literals over Σ1 ∪ Σ2 . Then, the non-deterministic NO combination

method can be described in the following way. First, a satisfiability preserving
transformation called purification is used to transform Γ into Γ1 ∧ Γ2 , such that, the
a a
symbols from Γi are in Σi , where Σi = Σi ∪ a, and a (= V(Γ1 ) ∩ V(Γ2 )) denotes the
set of shared variables between Γ1 and Γ2 . Then, a partition of a into disjoint subsets
is guessed and is expressed as a conjunction of literals φ. For example, the partition
{x1 }, {x2 , x3 }, {x4 } is represented as x1 6' x2 , x1 6' x4 , x2 6' x4 , x2 ' x3 . Then, the
individual procedures are used to decide whether Γi ∧ φ is satisfiable. The combined
procedure returns unsatisfiable if one of the procedures returns unsatisfiable.
For convex theories, instead of guessing, one can deduce the equalities to be
shared. The key idea is to propagate x ' y to Γ2 whenever T 1 ∪ Γ1 |= x ' y, and
vice-versa. This process is repeated until no further equations can be propagated.
Then, the individual procedures are used to decide whether Γi is satisfiable. Sharing
equalities in this case is sufficient, because a theory T 1 can assume that xM2 6= y M2
whenever x ' y is not implied by T 2 and vice versa. So, for convex theories, there
is an efficient way to construct a partition of the set of shared variables.

3 Related Work
3.1 Convex theories only
For convex theories it is sufficient to propagate all implied equalities between shared
variables. For instance, theories that admit canonizers solve equality propagation
by rewriting. In general, a theory T i is canonizing (as coined in [4]) if it admits a
function ↓ , such that:

T i ∪ Γi |= s ' t iff s ↓Γi = t ↓Γi .

Linear rational arithmetic is convex, procedures based on the Fourier-Motzkin

algorithm produce all implied equalities in a straight-forward way, but the procedure
may require exponential space. For procedures based on the Simplex algorithm, all
implied equalities can be deduced using the approaches described in [5,6].
The main disadvantage of these approaches is poor performance (either of the
solver or of the equality propagation) and the inability to deal with non-convex
theories.

3.2 DTC: Delayed Theory Combination

Several SMT solvers [7] use the underlying SAT solver to guess a partition of V(Γ1 )∩
V(Γ2 ), the idea is to create a literal u ' v for every pair of shared variables u
and v. One may be concerned that guessing a partition would be exponentially
more expensive than deriving it when the theories are convex. However, as shown
in [8], back-jumping and lemma learning allow simulating the standard Nelson-
Oppen combination method: equalities that are implied by a theory, once learned
are not flipped.
The obvious disadvantage of this approach is that the number of additional
equality literals is quadratic in the number of shared variables. There is an addi-
3
 de Moura, Bjørner

tional assumption that may be tool specific to MathSat, but are pervasive in the
results from [8]: all literals used by the SAT solver must be present in the input to
the SAT solver. At the current time of writing CVC3 [9], Verifun [10], Yices [11],
and our tool Z3 all support dynamically added literals.
Our approach, presented later, appeals to an SMT solver that allows introducing
literals on the fly. If this is not possible, the approach boils down to a branching
heuristic on top of DTC.

3.3 Ackermannization

When combining two theories T 1 and T 2 , where T 1 is the theory of uninter-

preted functions, one can eliminate T 1 by creating all ground instances of Leibniz’s
rule [12]:
^
ni ' mi → f (n) ' f (m) (1)
Thus, we can eliminate a function symbol f from a set of formulas F by applying
the procedure ackermannize:
ackermannize(f, F ) :
foreach f (n) ∈ F where n do not contain f
create a fresh constant af (n)
replace f (n) by af (n) in F
foreach af (n) , af (m)
V
add the clause ni ' mi → af (n) ' af (m) to F

A partial Ackermann’s reduction heuristic is proposed and investigated in [13].

Functions are only eliminated when the number of distinct occurrences is smaller
than the set of shared variables in the function arguments.
Ackermannization has the same disadvantage as DTC in that the number of
additional literals is quadratic in the size of the input. It is furthermore problematic
to use Ackermannization in the context of several theories and when combining SMT
solvers with quantifier instantiation.

3.3.1 Dynamic Ackermannization

Congruence closure algorithms for deduction in equational theories are ubiqui-
tous. Efficient and incremental congruence closure based procedures are described
in [6,14]. However, these algorithms miss the following propagation rule:
_
f (n) 6' f (m) =⇒ ni 6' mi . (2)
This propagation rule (which is a contrapositive of (1)) has a dramatic performance
benefit in some benchmarks, and Ackermann’s reduction gives this rule for free.
For example, the following simple formula takes O(2N ) time to be solved using the
algorithms presented in [6,14]. In contrast the formula can be solved in polyno-
mial time if either O(N 2 ) axioms are added up front by ackermannize or the above
propagation rule is used resulting in “only” O(N ) space and time overhead.
4
 de Moura, Bjørner

N
^
(pi ∨ xi ' v0 ) ∧ (¬pi ∨ xi ' v1 ) ∧ (pi ∨ yi ' v0 ) ∧ (¬pi ∨ yi ' v1 ),
i=1
f (xN , . . . , f (x2 , x1 ) . . .) 6' f (yN , . . . , f (y2 , y1 ) . . .) (3)
This performance problem reflects a limitation in the current congruence closure
algorithms used in SMT solvers, and it is not related with the theory combination
problem. In fact, the formula above uses only one theory. In [11], an approach,
called Dynamic Ackermannization, is proposed to cope with this problem. There,
clauses corresponding to Ackermann’s reduction are added when a congruence rule
participates in a conflict.

4 Model-based Theory Combination

Our approach minimizes the number of produced shared equalities. It is based on
the fact that, in practice, the number of local inconsistencies is much bigger than the
number of global (cross theory) inconsistencies. It works for convex and non-convex
theories alike.
(i) Each theory T i maintains a model Mi for Γi , or at times only for a subset of
Γi .
(ii) From time to time, if uMi = v Mi , then the theory creates the case-split u ' v,
the positive case is tried first.
(iii) At the discresion of the theory solver, change a model Mi to M0i to satisfy
newly assigned literals, or to imply fewer equalities.
It is fairly straight-forward to integrate this approach in a DPLL(T ) framework,
that we rename DPLL(T M ), as the search is now model-guided. Borrowing notation
from [15,16], the relevant new rules are presented in Fig. 1. The full set of rules
are repeated from [16] in Fig. A.1. The transition rules modify triplets of the form
M, Γ || F , where M is a set of models for theories T 1 , . . . , T n , Γ is a set of asserted
literals, and F is a set of clauses. The rule M-Propagate creates a fresh equality
literal (u ' v)d when a model associated with one of the theories imply it, but
the equality is not present in the context Γ. The equality literal is pushed on Γ,
thus propagating the equality to all theories sharing variables u and v. The tag d
on the literal indicates that the literal may be negated during backtracking. The
M-Mutate rule allows changing models during backtracking search. For instance,
after applying Decide, a newly assigned literal `d may not be satisfied in the existing
models. We do not need to specify when M-Mutate is applied. In particular, theory
solvers are not required to maintain models for their contexts at all times during
a search. Models are only required when other case splits have been attempted.
For example, when using linear programming for an integer linear programming
problem, a simplex tableau may choose to delay introducing Gomory cuts to obtain
an integer interpretation until other constraints have been propagated.
We use the following optimizations to minimize even further the number of
necessary case splits. Let RM be an equivalence relation on V such that RM (u, v)
iff uM = v M . Let classes(R) be the set of equivalence classes induced by R.
(i) Opportunistic equality propagation: Equalities that can be inferred without
5
 de Moura, Bjørner

M-Propagate



 u, v ∈ V, (u ' v) 6∈ L

M, Γ || F =⇒ d
M, Γ(u ' v) || F if u Mi = v Mi



 add (u ' v) to L

M-Mutate n
M, Γ || F =⇒ M0 , Γ || F if M0 is some variant of M

Fig. 1. Model-based propagation

additional expense to the theory solver are always propagated eagerly. Section 5
gives an example of opportunistic equality propagation.
(ii) Postponing model-based equality propagation: we delay applying the rule
M-Propagate until case splits on already existing literals have been performed.
(iii) Model mutators, the idea is to use a function δ(Mk ) that returns a more diverse
model. More formally, |classes(RMk )| ≤ |classes(Rδ(Mk ) )|

5 Simplex: An example model-producing theory solver

Following [17], a theory solver for linear arithmetic, and integer linear arithmetic,
can be based on a Simplex Tableau of the form:
X
xi ' aij xj xi ∈ B,
xj ∈ N

where B and N denote the set of basic and nonbasic variables, respectively. In
addition to this tableau, the solver state stores upper and lower bounds li and ui
for every variable xi and a mapping β that assigns a rational value β(xi ) to every
variable xi . The bounds on nonbasic variables are always satisfied by β, that is, the
following invariant is maintained
∀xj ∈ N , lj ≤ β(xj ) ≤ uj .
Bounds constraints for basic variables are not necessarily satisfied by β, so for
instance, it may be the case that li > β(xi ) for some basic variable xi , but pivoting
steps can be used to fix bounds violations, or detect an infeasible tableau. We hope
it does not come as a total surprise that the current model for the simplex solver
is given by β. Enumerating the equalities implied by β is simple: enumerate all
the values of β(xi ), inserting each value into a hash table. The expected time of
enumerating all equalities is then O(|B ∪ N |).

5.1 Opportunistic equality propagation

P
A variable xi is fixed iff li = ui , a linear polynomial xj ∈V aij xj is fixed iff for every
P
xj ∈ V, xj is fixed or aij = 0. Given a linear polynomial P = xj ∈V aij xj , we use
P
β(P ) to denote xj ∈V aij β(xj ).
FixedEq
6
 de Moura, Bjørner

li ≤ xi ≤ ui , lj ≤ xj ≤ uj =⇒ xi ' xj if li = ui = lj = uj

EqRow
xi ' xj + P =⇒ xi ' xj if P is fixed, and β(P ) = 0

EqOffsetRows 
xi ' xk + P1  P1 and P2 are fixed, and
=⇒ xi ' xj if
xj ' xk + P2  β(P ) = β(P )
1 2

EqRows 
xi ' P + P1  P1 and P2 are fixed, and
=⇒ xi ' xj if
xj ' P + P2  β(P ) = β(P )
1 2

The first rule can be implemented using a mapping from values to fixed variables,
the second rule can be easily checked when a row is updated during a pivoting step.
The rule EqOffsetRows is a simpler and less expensive version of EqRows. It can
be implemented using a mapping (xk , v) 7→ xi , where xk and xi are variables, and
v is a value. In our implementation, the first three rules are eagerly applied, and
the last one is only applied before M-Propagate. We also aggressively remove fixed
variables from the basis.
These rules can miss some implied equalities. For instance, from the con-
straints (4), the rules detect the implied equality z ' w, but miss the equality
x ' y, because z is not a fixed variable. Fortunately, the bound propagation tech-
nique described in [17] can be used imply the bound 0 ≤ w, making w a fixed
variable, and enabling the application of the rule EqRow.
x ' y + w + s, z ' w + s, 0 ≤ z, w ≤ 0, 0≤s≤0 (4)

5.2 Mutation using freedom intervals

The freedom of a non-basic variable xj is defined as the interval [Lj , Uj ], where:

    
li − β(xi ) ui − β(xi )
Lj = max β(xj ) + | aij > 0 ∪ β(xj ) + | aij < 0 ∪ {lj }
aij aij
    
ui − β(xi ) li − β(xi )
Uj = min β(xj ) + | aij > 0 ∪ β(xj ) + | aij < 0 ∪ {uj }
aij aij
Intuitively, if β satisfies all rows and bound constraints, then β will also satisfy
them after executing update(xj , v) for any value v in the interval [Lj , Uj ], where the
update procedure is defined as:

update(xj , v)
foreach xi ∈ B, β(xi ) := β(xi ) + aij (v − β(xj ))
β(xj ) := v

7
 de Moura, Bjørner

Freedom intervals can be used to produce a more diverse β without performing any
pivoting operation. A simple greedy heuristic seems to be quite effective: for each
non-basic variable xj , execute update(xj , v), if there is a value v ∈ [Lj , Uj ] such that
|classes(Rβ )| < |classes(Rβ 0 )|, where β 0 denotes β after the update operation.

6 Experimental Evaluation
The experiments were conducted using a 32bit Pentium 4 processor running at
3.6Ghz, 2Gb of memory, and 2Mb of cache. The timeout was set to 10 minutes. We
compared our approach against other SMT solvers and against different strategies
within our solver Z3. We used the same benchmarks used in [13]. The benchmarks
were translated to the SMT-LIB format, and are available for download in our
website 3 . We also included, for N ∈ [1, 99] the examples from (3) and the following
simple family of satisfiable formulas in the comparison for N ∈ [2, 99]:
N
^
ϕ= f (xi ) ≥ 0 ∧ xi ≥ 0 ∧ xi 6' xi+1 (5)
i=1
All benchmarks but the Ackermann suite use the theories of uninterpreted functions
and linear arithmetic. Tables 1 and 2 summarize the results obtained in our ex-
periments. Each cell has the accumulated time, in seconds, used by each solver to
solve a family of benchmarks. It does not include the time spent in instances where
the solver produced the unknown result. A solver is considered to have produced
the unknown result when it times out or crashes. The number of unknown results
is displayed using parenthesis. MathSAT-dtc denotes the MathSAT solver with the
command line option -DTC that forces it to use Delayed Theory Combination. We
used Yices version 1.0.8 in the experiments. Yices is also based on DTC, but the
shared equalities are lazily generated, and it uses a filtering mechanism to avoid
the generation of unnecessary shared equalities [11]. Yices and Z3 implement Dy-
namic Ackermannization suggested in [11]. Six different versions of our Z3 solver
were used: Z3-dtc uses delayed theory combination and the additional equalities be-
tween shared variables are eagerly generated; Z3-dtc* is similar to Z3-dtc but uses
the current model to implement a branching heuristic for the generated equalities;
Z3-ack uses Ackermann’s reduction as a pre-processing step; Z3-neq, Z3-ndack and
Z3 all use Model Based Theory Combination, but Z3-neq does not use opportunis-
tic equality propagation, and Z3-ndack does not use Dynamic Ackermannization.
Notice that our implementation of Z3-dtc does not include several optimizations
that may be useful for a DTC framework. It does not take advantage of theory
propagation for arithmetic.
The benchmarks in the EufLaArithmetic family are trivial if the linear arithmetic
solver performs some form of opportunistic equality propagation. The Simple family
described above was used to demonstrate that DTC is not robust. Yices performs
poorly on most satisfiable instances in the RandomCoupled and RandomDecoupled
families.
Model based theory combination seems to be more robust than DTC or Ack-
ermann’s reduction. In these benchmarks, the average number of shared equalities
3 http://research.microsoft.com/∼leonardo/SMT07

8
 de Moura, Bjørner

# MathSAT MathSAT-dtc Yices Z3

EufLaArithmetic 52 1851.50 (11) 785.87 (1) 10.45 17.34
Hash 199 520.90 19.39 11.48 6.54
Wisa 256 886.36 (1) 6916.18 4.37 2.78
RandomCoupled 400 517.05 518.15 9516.11 (51) 56.16
RandomDecoupled 500 11989.60 (1) 97.07 19362.40 (51) 41.95
Simple (5) 98 1366.33 7053.98 (29) 2328.63 (53) 1.00
Ackermann (3) 99 228.49 (82) 344.00 (82) 2.99 1.72
Total 1604 17360.23 (95) 15734.64 (112) 31236.43 (155) 127.49

Table 1
Experimental results

Z3-dtc Z3-dtc* Z3-ack Z3-neq Z3-ndack Z3

EufLaArithmetic 796.71 (11) 2830.38 (4) 1094.47 (1) 786.15 11.56 17.34
Hash 310.10 305.75 23.68 5.89 6.02 6.54
Wisa 364.71 385.06 12.31 4.89 2.40 2.78
RandomCoupled 8122.45 (166) 12451.82 (103) 101.24 56.45 56.65 56.16
RandomDecoupled 12421.30 (85) 15316.60 (71) 56.54 51.23 48.39 41.95
Simple (5) 7.26 7.34 33.89 0.45 1.00 1.00
Ackermann (3) 728.22 (77) 733.58 (77) 37.99 1.74 874.21 (77) 1.72
Total 22750.75 (339) 32030.53 (255) 1360.12 (1) 906.78 1000.23 (77) 127.49

Table 2
Experimental results (only Z3)

propagated by Z3 using M-Propagate was 2.46. The maximum was 57.

7 Conclusions
This paper introduced a new approach for dealing with equality propagation in
the context of convex theories where equality deduction is expensive and more
generally, in the context of non-convex theories. Both in theory, and as we validated
experimentally, the approach solves a number of practical deficiencies with other
known solutions to integrating theories.
Model-based Theory Combination requires that a decidable theory maintains a
notion of a model that supports efficiently answering queries of the form uM = v M .

7.1 On the significance of Ackermann’s reduction

The Wisa benchmark set is used in [13] to illustrate the usefulness of Ackermann’s
reduction in contrast with DTC. With Model-based Theory Combination, Acker-
mann’s reduction does not help on these set of benchmarks. We therefore believe
they reflect more the problems with DTC than the advantages of Ackermann’s
reduction. On the other hand, the synthetic Ackermann benchmarks, one can ob-
serve the utility of the reduction. Dynamic Ackermann reduction is not without
an overhead: new literals are added to the search space, and the new literals cause
T-Propagate to spend additional overhead of walking use-lists. Future work includes
investigating whether it is a practical advantage to build in the propagation directly
into a congruence closure algorithm.
9
 de Moura, Bjørner

7.2 Are theories amenable to Model-based combinations?

Our main example of a model producing theory solver was a classical Simplex solver.
We are experimenting with adding model-based solvers to other theories, and we
hope to be reporting on our findings in future work.

8 Acknowledgment
The authors would like to thank Alberto Griggio for providing the latest version of
MathSAT and adding a command line option for enabling Delayed Theory Combi-
nation.

References
[1] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., van Rossum, P., Schulz, S., Sebastiani, R.:
The MathSAT 3 System. In Nieuwenhuis, R., ed.: CADE. Volume 3632 of Lecture Notes in Computer
Science., Springer (2005) 315–321

[2] Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12 (1980)
291–302
[3] Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on
Programming Languages and Systems 1(2) (1979) 245–257

[4] Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1) (1984) 1–12

[5] Rueß, H., Shankar, N.: Solving linear arithmetic constraints. Technical Report SRI-CSL-04-01, SRI
International (2004)

[6] Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3)
(2005) 365–473

[7] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.:
Efficient theory combination via boolean search. Inf. Comput. 204(10) (2006) 1493–1525

[8] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: Delayed Theory Combination vs.
Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis. In: LPAR. (2006) 527–541

[9] Barrett, C., Tinelli, C.: CVC3. In: CAV ’07. (2007) to appear.

[10] Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical
Report HPL-2004-199, HP Laboratories, Palo Alto (2004)

[11] Dutertre, B., de Moura, L.: The Yices SMT Solver. http://yices.csl.sri.com/tool-paper.pdf (2006)

[12] Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundation of
Mathematics (1954)

[13] Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Santuari, A., Sebastiani, R.: To Ackermann-ize
or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in UF(E). In:
LPAR. (2006) 557–571

[14] Nieuwenhuis, R., Oliveras, A.: Fast Congruence Closure and Extensions. Inf. Comput. 2005(4) (2007)
557–580
[15] Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision
procedures. In: CAV 04. LNCS 3114 (2004) 175–188

[16] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract
Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6) (2006) 937–977

[17] Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: CAV’06. LNCS 4144,
Springer-Verlag (2006) 81–94

[18] Sheini, H.M., Sakallah, K.A.: SMT(LU): a step toward scalability in system verification. In Hassoun,
S., ed.: ICCAD, ACM (2006) 844–851

10
 de Moura, Bjørner

A A presentation of DPLL(T M )
Fig. A.1 repeats from [16] the presentation of DPLL(T ) as an abstract transition
system. We have added M to each sequent to emphasize that the current state
during proof-search also carries a model. In contrast to [16], we use a set L of literals
to choose case split candidates from. We assume L is a super-set of the literals
occurring in the set of clauses F . Besides the fresh equality literals introduced by
the rule M-Propagate, non-convex theory implementations, such as an integer linear
solver may introduce fresh literals as a side-effect of performing branch-and bound
search.

11
 de Moura, Bjørner

UnitPropagate 
 Γ |= ¬C
M, Γ || F, C ∨ ` =⇒ M, Γ` || F, C ∨ ` if
 ` is undefined in Γ

Decide 
 ` occurs in L
M, Γ || F =⇒ M, Γ`d || F if
 ` is undefined in Γ

Fail 
 Γ |= ¬C
M, Γ || F, C =⇒ fail if
 Γ contains no decision variables

Backjump



 Γ`d Γ0 |= ¬C,


there is a clause C 0 ∨ `0 such that





M, Γ`d Γ0 || F, C =⇒ M, Γ`0 || F, C if F, C |= C 0 ∨ `0 and Γ |= ¬C 0 ;


`0 is undefined in Γ;






 0
` or ¬`0 occurs in F or in `d Γ0


T-Propagate



 Γ |=T `

M, Γ || F =⇒ M, Γ` || F if ` occurs in L



 ` is undefined in Γ

Learn 
 all atoms of C occur in L
M, Γ || F =⇒ M, Γ || F, C if
 F |= C
T

Forget n
M, Γ || F, C =⇒ M, Γ || F, C if F |=T C

Restart
M, Γ || F =⇒ M, ∅ || F

Fig. A.1. DPLL with exhaustive theory propagation

12