Satisfiability Modulo Theories
------------------------------
Many problems from program analysis involving data structures and
arithmetic can be reduced to checking logical formulas for
satisfiability. In the case where the atomic formulas belong to a
particular theory and the nesting depth of quantifiers is moderate one
speaks of *satisfiability modulo theories* (SMT). SMT can be seen as a
generalisation of propositional satisfiability with propositional
letters now being atomic formulae of a given theory.
For a simple example consider the classic
SEND
+MORE
------
MONEY
we can introduce eight integer variables D, E, M, N, O, R, S, Y and
for each variable x the constraints 0<=x, x<=9 and then the constraint
1000*S + 100*E + 10*N + D
+ 1000*M + 100*O + 10*R + E
=10000*M + 1000*O + 100*N + 10*E + Y
This is merely a conjunction of atomic formulas in linear integer
arithmetic (LIA) and can be solved using any SMT-Solver, e.g. Z3 or
Yices in no time.
E.g. in Yices
(define D::int)(define E::int)(define M::int)(define N::int)
(define O::int)(define R::int)(define S::int)(define Y::int)
(assert (<= 0 D))(assert (<= 0 E))(assert (<= 0 M))(assert (<= 0 N))
(assert (<= 0 O))(assert (<= 0 R))(assert (<= 0 S))(assert (<= 0 Y))
(assert (>= 9 D))(assert (>= 9 E))(assert (>= 9 M))(assert (>= 9 N))
(assert (>= 9 O))(assert (>= 9 R))(assert (>= 9 S))(assert (>= 9 Y))
(assert (=
(+ (+ (* 1000 S) (* 100 E) (* 10 N) D)
(+ (* 1000 M) (* 100 O) (* 10 R) E))
(+ (* 10000 M) (* 1000 O) (* 100 N) (* 10 E) Y)))
(check)
(show-model)
Examples from my own research.
1) Automatic complexity analysis. Determine coefficients in such a way
that certain implications between inequalities become true.
2) Probabilities and higher-order functions. In order to show a
certain important conjecture (not finished yet) one needs to define
operations on triples of real numbers using addition and maximum and
show that these enjoy certain properties, e.g.\ transitivity,
commutativity, etc. SMT also very useful here for the generation of
counterexamples ...
First-order theory
- - - - - - - - - -
We assume known basic definitions about first-order logic. Signatures,
formulas, atomic-formulas, predicate symbols, function symbols,
quantifiers, quantifier-free formulas, structures, interpretation,
model. We always use first-order logic with equality.
A first-order theory over some signature (of can be defined as a class
of structures stable under isomorphism in the sense that if A is a
structure in the theory and A' arises from A by consistently renaming
the elements of the carrier set (A' is isomorphic to A) then A' is in
the theory, too. An element of a theory T is usually called a model of
T or T-model.
Often, theories are given implicitly by a set of closed formulas thus
comprising the structures satisfying this set. If T is a theory and
phi a closed formula one writes T |= phi to mean that every model of T
satisfies phi. If phi is a formula with free variables then T |= phi
means T |= all xs.phi. In either case, we say that phi is valid in T
or T-valid, for short.
Examples: the theory of groups, linear arithmetic, equality, equality
with uninterpreted function symbols.
E.g. if TG is the theory of groups over the signature (*,e) then
T |= all x.ex y.x*y=e /\ all x y z. x*(y*z) = (x*y)*z
For the theory UF of equality and uninterpreted function symbols one has
UF |= f(f(f(f(f(x))))) = x & f(f(f(x))) = x => f(x)=x
For the theory UFLIA of linear arithmetic together with uninterpreted
function symbols f one has
UFLIA |= x<=y+1 & y>=x-1 & z=f(x) & w = f(y+1) => w=z
Often, free variables are also understood existentially. We notice
that a quantifier free phi holds in T, written T |= phi, if there does
not exist a T-model M and a valuation eta of the free variables in phi
such that M,\eta |= ~phi. Such a pair consisting of a T-model and a
valuation of the free variables is called a T-model of ~phi. We thus
have that T |= phi iff there does not exist a T-model of ~phi. The
existence of a T-model is called T-satisfiability. Formulated
contrapositively, T |= phi fails to hold if there is a T-model of
~phi, i.e., if -phi is T-satisfiable. Often, one is also interested in
models in their own right, for example, when one seeks a solution for
a system of constraints like the "send more money" puzzle above.
Summary: T |= phi means T |= all xs.phi
phi T-satisfiable means that there is M,eta such that M,eta |= phi.
T |= phi iff -phi is T-unsatisfiable
phi is T-satisfiable iff T |= -phi fails to hold.
Definition: A theory T is stably infinite if every T-satisfiable
quantifier-free formula has a countably infinite T-model.
Formulated contrapositively, T is stably infinite if whenever a
quantifier-free formula holds for all countably infinite models then
it is T-valid.
Literals and clauses
- - - - - - - - - - -
An atomic formula has the form P(t1..tn) for P a predicate symbol or
t=t'. A literal is an atomic formula or a negated atomic formula. If
l is a literal then ~l denotes the negated literal,
e.g. ~(~P(ts))=P(ts).
A clause is a disjunction of literals. A cube or minterm is a
conjunction of literals. Every quantifier-free formula can be written
as a conjunction of clauses (CNF) and often problems are already in
this form. Dually, any quantifier-free formula can be written as a
disjunction of cubes (DNF). A CNF is T-valid iff each of its clauses
is T-valid; a DNF is T-satisfiable iff each of its cubes is.
The clausal validity problem (CVP) for a theory T is to determine
whether a given clause is T-valid or equivalently if a given cube
(conjunction of nonnegated or negated atomic formulas) is
T-satisfiable.
For many theories, in particular EQ, LIA, UFLIA, UF the CVP is
efficiently decidable. For a simple example, let us consider the
special case of linear arithmetic with equations only (no
inequalities). A clause can be written in the form
/\_i s_i = t_i => \/_j u_j = v_j
it is valid iff /\_i s_i = t_i => u_j = v_j holds for each j
(convexity of equational theories). The latter can be tested by
solving the solving the equations (parameter form) and plugging in.
If a theory has CVP then (by bringing to CNF or DNF as appropriate)
validity and satisfiability of arbitrary quantifier-free formulas is
decidable. If, however, in the case of satisfiability, the formula is
not a DNF (in particular, when it is given as a CNF!) then this will
incur an exponential overhead
Satisfiability modulo theories (SMT) is aimed at making this more
efficient in practice by harnessing the methods of propositional
SAT-solving.
Definition: A theory T is convex if whenever a cube implies a
disjunction of equations then it implies one of the disjuncts.
All equational theories (defined by universally-quantified equations,
e.g. groups, linear equations) are convex. This means that for those
the CVP reduces to validity for Horn clauses, i.e., implied equations.
The theory of fields is not convex:
xy=0 => x=0 \/ y=0 is valid, but neither xy=0 => x=0 nor xy=0 => y=0 are.
CVP for Equality and UF
- - - - - - - - - - - -
The theory EQ has merely variables and equations between them. CVP for
these can be efficiently solved using the union-find algorithm:
Compute the equivalence relation generated from the equations and see
whether this contradicts one of the disequations.
For example, x=y,y=z,z=u,x!=u is unsatisfiable because x=u follows.
The theory UF just has function symbols and equality. Its CVP can be
reduced to that for EQ using Ackermann's method: introduce
abbreviations for subterms so that each equation takes the form x=y or
f(xs)=y. Then add boolean congruence axioms and remove all equations
and disequations containing function symbols. The resulting boolean
formula over EQ is equisatisfiable.
Example: f^5(x)=x, f^3(x)=x, f(x)!=x.
Introducing abbreviations:
f(x)=a,f(a)=b,f(c)=d,f(d)=e,f(e)=g,g=x,d=x,a!=x
Congruence axioms:
x=a => a=b, x=c => a=d, x=d => a=e, x=e => a=g, a=c => b=d etc etc.
A more efficient method is known as congruence closure.
CVP for Linear Arithmetic
- - - - - - - - - - - - -
Here we want to show that linear arithmetic (LIA) admits efficient
CVP. The terms of LIA are built up from variables by addition and
multiplication with rational constants. The predicate symbols = and
<=.
Note that >=, <, > can be defined using negation and symmetry.
Let x be the vector of variables occurring in a given cube. Let n be
its dimension.
Using basic arithmetic manipulations we can
transform the cube into a conjunction of formulas
u^T x <= b for u:QQ^n and b:QQ
u^T x < b for u:QQ^n and b:QQ
Now u^T x < b is equivalent to u^T + delta <= b for some delta > 0 and
for each of the strict inequalities we can use w.l.o.g. one and the
same delta.
We thus reduce CVP to the following question: Given an mxn matrix A and a vector b:QQ^n does there exist a vector x:QQ^m such that
A x <= b
and such that one particular component of x is >0.
This, however, can be efficiently found out using the simplex
algorithm. Just maximize the objective function x |-> delta /* the
"particular component"*/ subject to Ax <= b and see whether the
optimum is >0.
The Nelson-Oppen combination
- - - - - - - - - - - - - - -
Let T1 and T2 be theories over disjoint signatures, i.e. the only
common symbol is equality.
Example: T1 = LIA, T2 = UF.
We then form the combined theory T1+T2 whose models are those
structures which (after forgetting the interpretation of the
superfluous symbols) are models of both T1 and T2.
Nelson-Oppen: If T1 and T2 are stably infinite and convex then if CVP
is decidable for T1 and T2 then CVP is decidable for T1+T2.
Let us first see that CVP for T1+T2 is not altogether trivial,
i.e. that there may be some interaction between T1 and T2 albeit only
through equality. E.g., in LIA+UF we have f(x-1)-1 = x+1, f(y)+1=y-1,
y+1=x => 0=1
Coming back to the CVP for T1+T2, we can equivalently test a T1+T2 cube
for satisfiability. By introducing abbreviations for subterms we can
(in linear time) bring such a cube into the equisatisfiable (!) form
Phi & Psi where Phi is a T1-cube and Psi is a T2-cube. This is known
as *purification*.
In the example, we could take
w=f(z), u=f(y), z=x-1, w-1=x+1, u+1=y-1, y+1=x, 0 != 1
Thus, Phi is z=x-1, w-1=x+1, u+1=y-1, y+1=x, 0!=1 and Psi is w=f(z),
u=f(y), z=x-1, w-1=x+1, u+1=y-1, y+1=x, 0!=1
Now let V = FV(Phi) & FV(Psi) be the set of variables occurring in
both Phi and Psi (in the example V={w,z,u,y}).
We begin by checking which equations between variables in V are
implied by Phi. We then add those equations to Psi and see what more
equations are then entailed by Psi. After that we try again with Phi
and so forth. Since each new equation reduces the number of hitherto
unrelated variables (the number of equivalence classes) the process
will stabilise after |V| rounds with a set of equations E between
variables in V such that
1) T1+T2 |= Phi,Psi => E /* all equations in E are consequences of Phi,Psi*/
2) If T1 |= Phi,E => x=y for some x,y:V then x=y is contained in E
3) If T2 |= Psi,E => x=y for some x,y:V then x=y is contained in E
Main result of Nelson-Oppen method: Phi,Psi is satisfiable in T1+T2
if and only if Phi,E is satisfiable in T1 and Psi,E is satisfiable in T2.
We sketch a proof of this:
Condition 1 ensures the only if direction. For the other direction define
E' = {"x != y" | "x=y" not in E}
as the set of all disequations between variables in V whose equality
is not explcitly asserted in E.
If Phi,E is satisfiable, so is Phi,E,E'. To see this, note that
otherwise, we would have Phi,E |= \/{"x=y" | "x=y" not in E} and then,
by convexity, Phi,E |= x=y, for some equation x=y not in E. By
condition 2), this had been ruled out. Likewise, Psi,E,E' is
satisfiable (using condition 3). So, let M1 be a T1-model of Phi,E,E'
and M2 be a T2-model of Psi,E,E'. Since T1,T2 are stably infinite, we
can assume that M1 and M2 are countably infinite and w.l.o.g. both
have the natural numbers for carrier set. Now apply a permutation to
the carrier set of M1 so that the interpretations of the variables in
V coincide in M1' and M2. The addition of E' ensures that this is
possible (otherwise, it could have been that M1 equates x and y but M2
doesn't). The combination of the interpretations of variables and
symbols from M1' and M2 then gives the desired T1+T2 structure
satisfying Psi,Phi.
In this way, we obtain decidable CVP for many of the combined theories
that are of interest in practice. In the literature, one finds
generalisations of Nelson-Oppen relaxing the preconditions and also
more efficient versions for special cases, e.g. Shostak's method.
We also remark that without the convexity restriction, the
communicating formula E must be chosen as a disjunction of equations
resulting in an exponential overhead and a more complicated proof.
Using SAT Solvers for SMT
- - - - - - - - - - - - -
We now assume a theory T with decidable CVP and are interested in
deciding satisfiability of an arbitrary quantifier-free formula. By
the usual encodings the formula can be assumed in CNF (for which
satisfiability is "difficult").
A black-box SAT solver (checks propositional CNF for satisfiability)
can be used as follows.
1) Treat the atomic formulas of the CNF as propositional variables (as
in Herbrand's theorem). E.g. x=2y+f(z) becomes "x=2y+f(z)".
2) Run the SAT-Solver on the resulting propositional CNF.
3) If the SAT-Solver reports unsatisfiability then the CNF is also
T-unsatisfiable.
4) If the SAT-Solver gives a satisfying assignment, treat it as a cube
(conjunction of literals) and use the decision procedure to see
whether it is T-satisfiable (recall that clausal validity and
satisfiability of cubes is the same thing).
5) If yes, then the formula is T-satisfiable
6) If not, add the negation of the offending cube as a new clause and
start over.
Regarding 4), it might e.g. be that the SAT-Solver sets "x=y" and "y=z"
to true but "x=z" to false. In EQ this is not possible so we would at
this point add the clause "x!=y \/ y!=z \/ x=z".
A finer interaction with the inner workings of a SAT solver is also
possible in particular when it is based on the DPLL procedure with
conflict-driven clause learning (CDCL).
Let us recall the basic functioning of this procedure. Given a clause
set K to be tested for satisfiability the procedure maintains a
partial assignment eta and also a set of learned clauses C both
initialised to the empty set.
The current clause set K u C is aggressively simplified by unit propagation ...
* assignments from eta are plugged in: satisfied clauses are removed,
false literals are removed from clauses.
* resulting unit clauses are temporarily added to the assignment eta possibly
yielding more simplifications.
until either a contradiction is found or no more simplifications are possible.
Then an unset variable x is selected and tentatively set to a value.
If at any one point a conflict (empty clause) is found then in general
this does not mean that the CNF is unsatisfiable, only that one of the
tentative variable settings was wrong.
By analysing the derivation of the empty clause by unit propagation
one finds out which particular variable settings were needed. All
those and including all later ones (depending on them) must be
undone. The negation of the responsible settings can be added as a
learned clause to C. Say, the settings x=true, y=false, u=true were
responsible for the conflict. One then adds the clause ~x v y v ~u.
If all possibilities for setting variables are exhausted and no
satisfying assignment has been found then the original CNF is
unsatisfiable.
The Wikipedia page on Conflict-Driven Clause Learning contains an
illustrative example.
Various optimizations are possible in the implementation of unit
propagation ("watched literals"), the conflict analysis ("dependency
graphs"), and clause learning ("forgetting learned clauses from time
to time").
Now, using a CVP-solver for an underlying theory one can for example
also deduce new unit clauses during unit propagation. E.g., if x=y and
y=z are already available, we can add x=z even though this is not a
propositional consequence. Furthermore, before even starting with a
tentative variable setting we can use the CVP-solver to check its
consistency. E.g. if we have already set x=y to true and y=z to true
then setting x