§ Nondeterministic Nelson Oppen

§ Stably infinite thories

• A theory is stably infinite iff every satisfiable quantifier free formula is satisfiable in an infinite model.
• EUF and arithmetic are stably infinite.
• Bitvectors are not stably infinite, since they don't have infinite models. (i.e. the structure is itself finite)
• Theory of strings of bounded length (structure is finite).

§ Converting Formula to Separate Form

• Consider $1 \leq 2 \land f(x) \neq f(2) \land f(x) \neq f(1)$ in $T_E \cup T_Z$ (equality, integers).
• Separate, introduce new variable $y = 2, z = 1$.
• The array part becomes $f(x) \neq f(y) \land f(z) \neq f(z)$.
• The integer part becomes $1 \leq 2 \land y = 2 \land z = 1$.
• So, the two theories "communicate" via variables.

§ Theory Solvers need to coordinate

• Suppose we have $F = F_1 \land F_2$
• If either $F_1, F_2$ are are UNSAT, then $F$ is UNSAT.
• But if both $F_1, F_2$ are SAT, not guaranteed that the whole thing is SAT.

§ Coordinating Equivalence Relation

• Let $S$ be a set of terms with $\sim$ an equivalence relation.
• Then we write $F[\sim] \equiv (\land_{t \sim s} t = s) \land (\land_{t \not \sim s} t \neq s)$.
• For elements that are not related, we force disequality!

§ Non deterministic Nelson Oppen

• Take two disjoint theories $T_1, T_2$
• That is, theories $T_1, T_2$ with signatures $S_1, S_2$ such that $S_1 \cap S_2 = \emptyset$ so no common symbols.
• Let $F$ be a conjunction of literals from $T_1 \cup T_2$.
• Convert $F$ to separate form: $F_1 \land F_2$.
• Guess a coordinating. equivalence relation $\sim$ over $vars(F_1) \cap vars(F_2)$.
• Run $DP_1(F_1 \land F[\sim])$, and $DP_2(F_1 \land F[\sim])$.
• If both solvers are SAT, then return SAT, since we have found a common assignment.
• Otherwise, F is UNSAT.
• CLAIM: this is a correct algorithm!

§ Proof of correctness (Non-deterministic)

• For the proof, we need to know the reduct of a model to a smaller signature, and the notion of a model homomorphism.

§ Reduct of a model

• Let us a have a model $(M, S, T)$ where $M$ is the model, $S$ is the signature (tells us what the functions and predicates are), and $T$ is the theory (tells us what the axioms are.
• Then, for any subset $S' \subseteq S$, it's possible to build $(M, S')$ as a reduct of $(M, S)$.
• For example, $(Z, +, 0)$ is a reduct of $(Z, +, 0, 1, \times)$.

§ Thm1: Conjunct SAT iff they agree on intersection

• Let $F_1$ be an $S_1$ model, and $F_1$ has variables $V_1$ (mutatis mutandis for $F_2$).
• Claim: $F_1 \land F_2$ is satisfiable if and only if there exist $m_1 \models F_1$, $m_2 \models F_2$ such that $m_1 \sim m_2$ on $S_1 \cap S_2$(i.e. $m_1|_{S_1 \cap S_2, V_1 \cap V_2}$ is isomorphic as a $S_1 \cap S_2$ model to $m_2|_{S_1 \cap S_2, V_1 \cap V_2}$).

§ Proof (Large to small): $F_1 \land F_2$ SAT implies existence of $m_1, m_2$

• If $F_1 \land F_2$ is SAT, then there's a $S_1 U S_2$ model $M$. Let $m_1 \equiv M|_{S_1}$, (ditto $M_2$).
• Clearly, the restriction of the large model $M$ to $S_1$ will continue to model $F_1$, and ditto $F_2$, hence done.

§ Proof (small to large gluing): Isomrphic $m_1 \models F_1$ and $m_2 \models F_2$ implies existence of large model $M \models F_1 \land F_2$

• Idea: embed $(m_2, S_2)$ as a submodel of $(m_1, S_1)$ via the isomorphism $h$.
• This "just works", since they agree on the variables.
• Let $h$ be the iso $m_1 \sim_{S_1 \cap S_2} m_2$
• Let $M \equiv m_1$
• Let $M|S_1 = m_1$
• For $v_2 \in V_2, v \not in V_1$, define $M(v_2) \equiv h^{-1}(m_2(v_2))$.
• For $f_2 \in S_2, f \not in S_1$, define $M(f_2, a \in m_1 , \dots, z \in m_1) \equiv h^{-1}(f(h(a), h(b), \dots, h(z)))$.
• So we push $a, \cdots, z$ forward via $h$, evaluate $f_2$, then pull value back.

§ Meditation

• The key point is the sheaf-condition, which says that they agree on the intersection.
• Intuitively, this shows that we can form a pushout.

§ Thm2: Weaken Isomorphism To Cardinality + Equality Preservation

• Let $F_1$ be an $S_1$ model, and $F_1$ has variables $V_1$ (mutatis mutandis for $F_2$).
• Claim: $F_1 \land F_2$ is satisfiable if an only if there exist $m_1 \models F_1$, $m_2 \models F_2$ such that:
• (a) $|m_1| = |m_2|$ (underlying sets have same size)
• (b) For each variable $x, y \in V_1 \cap V_2$, we have that $m_1 \models x = y$ iff $m_2 \models x = y$.

§ Proof (Large to small): $M \models F_1 \land F_2$ implies existence of smaller models such that \dots

• Pick $m_1 = M|_{S_1}$, $m_2 = M|_{S_2}$. Clearly, same underlying set so same cardinality, and same model, so witnesses same equalities.

§ Proof (small to large gluing): Isomorphic $m_1 \models F_1$ and $m_2 \models F_2$ implies existence of large model $M \models F_1 \land F_2$

• Key idea: Since the models have the same cardinality, we can build the iso piecewise:
• Let $h : m_1[V_1 \cap V_2] to m_2[V_1 \cap V_2]$ be an empty iso from the values that $V_1 \cap V_2$ take in $m_1$ to the values that $V_1 \cap V_2$ take in $m_2$.
• Start by updating $h$ such that $h(m_1(v)) = m_2(v)$.
• This is injective, bcause suppose $h(m_1(v)) = h(m_1(v'))$. Then this means that $m_2(v) = m_2(v')$, which implies $m_1(v) = m_1(v')$, and thus we are done.
• The condition that $m_1 \models x = y$ iff $m_2 \models x = y$ ensures that $h$ remains an iso.
• This is onto since we've exhausted every variable in $V_1 \cap V_2$.
• Since $h$ is bijective, we have that $|m_1[V_1 \cap V_2]| = |m_2[V_2 \cap V_2]|$. Since |m 1| = |m 2|, this implies that we can extend $h$ arbitrarily to a bijective function on all of $m_1, m_2$.
• Clearly, by construction $h$ is an iso, and we thus apply previous theorm!

§ Meditation

• If we agree on variables, then we have the seed of an iso that witnesses that things are equal for ground formulae
• Then since we have same cardinality, we can extend to full iso!

§ Nelson Oppen Is Correct

• Let $T_1$ be stably infinite $S_1$ theory (mutatis mutandis).
• Let $F_1$ be a $S_1$ formula with variables $V_1$ (mutatis mutandis).
• Let $S_1 \cap S_2 = \emptyset$.
• $F_1 \land F_2$ is $T_1 \cup T_2$ satisfiable if and only if :
• There is an equivalence relation $\sim$ over $V_1 \cap V_2$ such that: $F_i \land F[\sim]$ is $T_i$ satisfiable.

§ Proof (large to small)

• Pick $M_1 = M|_{S_1, V_1 \cap V_2}$ and $M_2 \equiv M|_{S_2, V_1 \cap V_2}$, $x \sim y \iff x = y$.

§ Proof (small to large gluing):

• Suppose $\sim$ is equivalence relation such that $F_i \land F[~]$ is $T_i$ satisfiable.
• Since $T_1$ is stably infinite, we have infinite model $M_1 \models F_1 cap F[\sim]$.
• By downward lowenheim skolem, we have a countably infinite model $M_1$.
• So choose $M_1, M_2$ countable, thus $|M_1| = |M_2|$.
• Since $M_1 \models F[\sim]$ and $M_2 \models F[\sim]$, this means that $M_1(x) = M_1(x')$ if and only if $M_2(x) = M_2(x')$, because $F[\sim]$ asserts that all elements in the equivalence class are equal, and elements that are not in the equvalence class are not equal.
• Thus, we have that $M_1(x) = M_1(x')$ if and only if $x \sim x'$ if and only if $M_2(x) = M_2(x')$.
• TODO: I am not totally convinced here! I need to think :)

§ References

• Lecture 21-2 Correctness of Nelson-Oppen by Ashutosh Gupta
• Lecture notes on nelson oppen