Differences

This shows you the differences between two versions of the page.

--- sav08:combining_fol_models [2009/05/13 10:21]
vkuncak
+++ sav08:combining_fol_models [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== 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$.
-**Proof:** 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.**
-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.
-===== 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 [[ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/KrsGGT-TACAS-07.pdf|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:
-\[
-\le x \land x \le 2 \land y = 1 \land z = 2
-\]
-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)
-  * [[http://research.microsoft.com/projects/z3/smt07.pdf|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:
-  * [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]]
-===== References =====
-  * [[ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/NieOT-JACM-06.pdf|DPLL(T) paper]]