Convex Theory (Satisfiability Modulo Theory)

Definition

Convex Theory (Satisfiability Modulo Theory)

A theory $\mathcal{T}$ is convex if, for every finite conjunction $\Gamma$ of quantifier-free $\mathcal{T}$-literals and every finite non-empty family of equalities $u_j=v_j$,

$$\Gamma {\models }_{\mathcal{T}}\underset{j=1}{\overset{k}{\bigvee }}(u_j=v_j)⟹\exists j\in \{1,\dots ,k\}:\Gamma {\models }_{\mathcal{T}}(u_j=v_j).$$

Here $\Gamma {\models }_{\mathcal{T}}\phi$ means that every theory interpretation of $\mathcal{T}$ satisfying $\Gamma$ also satisfies $\phi$. Thus, whenever $\Gamma$ forces at least one equality in a finite disjunction, it already forces one particular equality from that disjunction.

Intuition

Think of $\Gamma$ as the constraints you have collected so far. A model is one way to satisfy them. Saying that $\Gamma$ forces an equality means that the equality holds in every remaining model, not merely in one solution you have found.

Start with an integer $x$ constrained by $0\le x\le 1$. You know that $x=0\vee x=1$. But do you know that $x=0$? No: $x=1$ is still possible. Do you know that $x=1$? No: $x=0$ is still possible. The disjunction is certain even though neither alternative is certain. This is exactly the behaviour that convexity forbids for equality consequences.

Now compare this with a convex theory. If a conjunction of literals guarantees $x=y\vee x=z$, then at least one of those equalities must already hold in every model of the conjunction. You do not have to choose an alternative and add it as an assumption: one alternative is already a consequence. Both may follow; convexity does not require exactly one.

The diagram makes this distinction visible. Reading across a row asks, “Does this model satisfy at least one equality?” Reading down a column asks, “Does this particular equality hold in every model?” Convexity says that whenever every row has a true entry, there must be an entirely true column.

Why the quantifier order matters: Let $M={\mathrm{Mod}}_{\mathcal{T}}(\Gamma )$ be the set of theory interpretations satisfying $\Gamma$, and abbreviate $u_j=v_j$ by $e_j$. Then

$$\begin{array}{rl}\Gamma {\models }_{\mathcal{T}}\underset{j=1}{\overset{k}{\bigvee }}{e}_j& ⟺\forall I\in M\exists j\in \{1,\dots ,k\}:I\models e_j,\\ \exists j\in \{1,\dots ,k\}:\Gamma {\models }_{\mathcal{T}}{e}_j& ⟺\exists j\in \{1,\dots ,k\}\forall I\in M:I\models e_j.\end{array}$$

In the first line, you may inspect the model before choosing $j$. In the second, you must choose one $j$ that works regardless of the model. Swapping these quantifiers is not valid in general; convexity is the property that makes this implication valid in this restricted setting.

What is being restricted? The requirement applies to every conjunction of theory literals and every finite non-empty disjunction of equalities that it entails. One successful instance does not prove that a theory is convex; one failing instance proves that it is not.

The restriction on $\Gamma$ matters. If arbitrary disjunctions were allowed as assumptions, we could simply assume $x=0\vee x=1$ even over the reals, without forcing either equality. Convexity does not prohibit disjunctions in SMT input; it describes what follows from conjunctions of literals inside a theory solver.

Nor does a convex theory need to determine a unique solution. In linear real arithmetic, $0\le x\le 1$ permits infinitely many values. Unlike the integer case, it does not entail $x=0\vee x=1$: $x=\frac{1}{2}$ refutes that disjunction. Here the premise of the convexity implication is false, so no particular equality needs to follow.

The disjunction must collapse

Suppose a constraint $\Gamma$ entails

$$u_1=v_1\vee u_2=v_2.$$

This says that every model of $\Gamma$ satisfies at least one of the two equalities. There are two possibilities:

1. the same equality holds in every model, for example $$\Gamma {\models }_{\mathcal{T}}{u}_1=v_1;$$
2. some models satisfy only $u_1=v_1$, while others satisfy only $u_2=v_2$.

A convex theory permits only the first situation whenever the disjunction itself is entailed. The theory need not force every disjunct, but it must force at least one fixed disjunct:

$$\text{forced disjunction of equalities}⟹\text{one forced equality}.$$

Convexity is therefore a semantic property of all relevant consequences of $\mathcal{T}$. It does not mean that the axioms of $\mathcal{T}$ must syntactically be conjunctions of literals.

Why Nelson–Oppen cares

In the Nelson–Oppen decision procedure, component solvers communicate equalities between shared variables. Suppose one solver derives only

$$x=y\vee x=z.$$

If its theory is convex, then it must actually derive $x=y$ or derive $x=z$. The solver can communicate that single equality to the other component.

If the theory is not convex, neither equality may follow individually. The other solver must then consider separate cases:

$$x=y\text{or}x=z.$$

Convexity therefore makes equality propagation sufficient. A Nelson–Oppen variant that enumerates complete equality arrangements can also handle non-convex theories, but it pays for this by branching over the alternatives.

Convexity and stable infiniteness solve different problems. Convexity prevents hidden disjunctive equality choices; stable infiniteness prevents incompatible domain cardinalities. The latter distinction is developed in Stable Infiniteness Removes Hidden Cardinality Conflicts.

Example

Linear integer arithmetic is not convex

Consider the linear-integer constraint

$$\Gamma :=(0\le x\wedge x\le 1).$$

Since $x$ is an integer, every model of $\Gamma$ assigns either $x=0$ or $x=1$. Therefore,

$$\Gamma {\models }_{\mathrm{LIA}}(x=0\vee x=1).$$

Neither equality follows individually:

$$\Gamma /{\models }_{\mathrm{LIA}}x=0\text{and}\Gamma /{\models }_{\mathrm{LIA}}x=1.$$

The assignment $x=1$ refutes the first entailment, while $x=0$ refutes the second. Hence, the forced disjunction does not collapse to one forced equality, so linear integer arithmetic is not convex.