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