Combining Decision Procedures

Merging Models of Theories with Disjoint Languages (Signatures)

Theorem: Let ${\cal L}$ be a finite language ${\cal L} = {\cal L}_1 \cup {\cal L}_2$ where ${\cal L}_1 \cap {\cal L}_2 = \emptyset$ . Let $C$ be a conjunction in language ${\cal L}$ , and for $i\in \{1,2\}$ let $C_i$ be those literals from $C$ whose symbols appear only in ${\cal L}_i$ , as well as equality and disequality literals. Suppose further that if variables $x,y \in FV(C_1)\cap FV(C_2)$ then either $x=y$ appears in $C$ or $x \neq y$ appears in $C$ (thus they also appear in $C_1$ and $C_2$ ). Let $Ax_i$ be a set of sentences in language ${\cal L}_i$ for $i\in\{1,2\}$ . Suppose there exists a model for $Ax_i \cup C_i$ for $i\in\{1,2\}$ and that these models have domains of same cardinality. Then there exists a model for $C \cup Ax_1 \cup Ax_2$ . Note: for $C$ to satisfy the condition, it suffices for it to be flat and to contain equality or disequality for all common variables. One possible way to achieve this is Atomic Diagram Normal Form but there is no need to do case analysis on literals other than equality literals.

Proof (using merging of models): There exists an isomorphism of interpretation $I_2$ such that the resulting structure $I'_2$ agrees with $I_1$ on the common variables. Extending $I_1$ with interpratation of symbols in $I'_2$ we obtain the desired model. End.

Proof (using interpolation): First-order logic has interpolation property, by Craig's interpolation theorem. Suppose we have models for $C_1 \cup Ax_1$ and $C_2 \cup Ax_2$ , but that there is no model for $C_1 \cup C_2 \cup Ax_1 \cup Ax_2$ . By compactness for first-order logic there exists a finite subset that is contradictory. By interpolation there exists an interpolant $I$ that is, say, implied by $C_1 \cup Ax_1$ and contradictory with $C_2 \cup Ax_2$ . The interpolant is in the common language, so it contains only equalities. It can be quantified, but over infinite domains quantifiers can be eliminated in a very simple way (and in any case, it is a fragment of BAPA that has QE). So, the result is a disjunction of conjunctions of equalities and disequalities among the common variables. But because $C_1$ and $C_2$ contain a complete atomic type, they either imply or are contradictory with $I$ , depending on whether the atomic diagram normal form contains the atomic type present in $C_1,C_2$ or not. Note that $I \cup C_2 \cup Ax_2$ is contradictory since $I$ is interpolant, so each conjunct in its DNF is contradictory. Therefore, $I$ does not have as a disjunct the atomic diagram present in $C_2$ or $C_1$ . Then $I$ is contradictory with $C_1$ as well. Since $I$ is a consequence of $C_1 \cup Ax_1$ , it follows that $C_1 \cup Ax_1$ is contradictory. But we assumed it is satisfiable. End

Example: Take formula

$\begin{equation*} x=1 \land f(x)=y \land z=y+y \land f(z)=x \land y \neq x \end{equation*}$

If we take a finite model for uninterpreted functions, we cannot merge it with the model for addition. But there is an infinite model for uninterpreted functions as well, and we can merge this model with the model for integers.

Stable Infiniteness

We wish to use different decision procedures to check $Ax_i \cup C_i$ satisfiability.

How do we know whether models have same cardinality?

decision procedure could tell us cardinality of model which it found (see Combined Satisfiability Modulo Parametric Theories)
we only work with theories that are guaranteed to have infinite models - stable infiniteness requirement

Definition: Theory $T$ is stably infinite iff for every quantifier-free formula $F$ , if $T \cup \{F\}$ is satisfiable then $T \cup \{F\}$ has an infinite model.

In practice this is not a restriction.

One way to ensure this: make sure that $T$ only has infinite models by adding axioms that there exists at least $k$ elements for all $k$ .

if we need to reason about some number of finitely many elements, add a unary predicate and look at elements that satisfy it

Example: The following theories are stably infinite:

integers, rationals (in fact, they have only infinite models, because they can define irreflexive total order)
uninterpreted function symbols: add fresh elements (they do not participate in satisfying assignment of quantifier-free formula)

Combining Decision Procedures By Guessing Arrangements

Suppose we have a collection of decision procedures for stably infinite theories.

Algorithm for deciding quantifier-free formulas in union of those theories:

generate a conjunction (using SAT solver)
flatten conjunction and separate it into different theories
guess an arrangement of equalities (this is additional case analysis)
apply decision procedure with its literals and the guessed arrangement

This method is complete for quantifier-free formulas:

if a decision procedure says UNSAT, the conjunction is UNSAT (because conjunctions given to theories are weaker than the entire conjunction)
if all conjuncts are UNSAT (for all arrangements, for all SAT disjuncts), the problem is UNSAT
if some conjunct, for some arrangement, is SAT for all decision procedures, then the Theorem above says that the entire conjunction is SAT, so problem is SAT

Convex Theories

Convex theories are theories that allow us to avoid guessing the arrangement.

Idea: instead of just checking SAT/UNSAT, the decision procedure will derive all equalities that follow from the conjunction.

In some cases there is no single equality that follows, but only a disjunction can be derived:

$\begin{equation*} 1 \le x \land x \le 2 \land y = 1 \land z = 2 \end{equation*}$

implies $x=y \lor x=z$ but not any other non-trivial equality between variables. We say integer linear arithmetic is a non-convex theory.

Definition: Theory $T$ is convex iff for every conjunction of literals $C$ , the condition $T \land C \models \bigvee_{i=1}^n (u_i=v_i)$ implies that there exists $i$ such that $T \land C \models u_i=v_i$ .

In short, a formula in convex theory implies a disjunction iff it implies one of the disjuncts.

Examples of convex theories

linear arithmetic over rational numbers
quantifier-free uninterpreted functions
quantifier-free term algebras

Equality Propagation

Instead of guessing arrangement, split the literals and let theories derive equalities and disjunctions of equalities, and propagate it to all other theories.

convex theories propagate only individual equalities
non-convex theories propagate disjunctions of equalities

This is the Nelson-Oppen technique for combining decision procedures.

To see completeness, consider the stage when no theory has new equalities or disjunctsions of equalities to report. Take the conjunction of negations of all remaining atomic formulas. We claim that this is satisfiable for all theories. Indeed, if it was not, then the negation of this conjunction would be implied by one of the theories.

Theory Propagation

Why derive only new equalities and rely on SAT solver to guess literals?

if theory concludes that a literal must be true, it selects it
can improve efficiency if the algorithm for theory anyway derives such information

Recent approach - try to propagate candidate equalities (even if they are not implied)

Model-based Theory Combination, Leonardo de Moura and Nikolaj Bjørner, Workshop on Satisfiability Modulo Theories (SMT), Berlin, Germany, 2007.

Complexity

if each theory is convex and polynomial time (e.g. congruence closure + real linear arithmetic), then conjunctions can be decided in PTIME
if each theory is NP (e.g. we also allow integer linear programming), then (even for non-convex theories), any quantifier-free combination is in NP

Theories with Non-Disjoint Languages

Essentially, what is shared between conjunctions of literals in languages in ${\cal L}_1$ and ${\cal L}_2$ is the equality symbol. If more than equality is shared, then interpolation theorem tells us that we may need to exchange quantified formulas. If we have quantifier elimination for the theory of shared signature, then it suffices to exchange quantifier-free formulas.

The correctness proof for Nelson-Oppen techniques in Calculus of Computation Textbook, Section 10.4 uses a proof of Theorem stated above that would generalize to the case of some other theories that admit quantifier elimination.

Proof idea:

FOL has interpolation property
if the formula is unsatisfiable, there exists an interpolant in language ${\cal L}_1 \cap {\cal L}_2$ , which generalizes the notion of arrangement for equalities
if we have quantifier elimination for formulas in ${\cal L}_1 \cap {\cal L}_2$ with respect to $T_1 \cup T_2$ , then arrangements are quantifier-free

Alternative method:

On Combining Theories with Shared Set Operations

References

DPLL(T) paper