Convex Theory (Satisfiability Modulo Theory)

Definition

Convex Theory (Satisfiability Modulo Theory)

A theory is convex if, for every finite conjunction of quantifier-free -literals and every finite non-empty family of equalities ,

Here means that every theory interpretation of satisfying also satisfies . Thus, whenever forces at least one equality in a finite disjunction, it already forces one particular equality from that disjunction.

Intuition

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

Start with an integer constrained by . You know that . But do you know that ? No: is still possible. Do you know that ? No: 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 , 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 be the set of theory interpretations satisfying , and abbreviate by . Then

In the first line, you may inspect the model before choosing . In the second, you must choose one 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 matters. If arbitrary disjunctions were allowed as assumptions, we could simply assume 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, permits infinitely many values. Unlike the integer case, it does not entail : 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 entails

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

1. the same equality holds in every model, for example
2. some models satisfy only , while others satisfy only .

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:

Convexity is therefore a semantic property of all relevant consequences of . It does not mean that the axioms of 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

If its theory is convex, then it must actually derive or derive . 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:

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

Since is an integer, every model of assigns either or . Therefore,

Neither equality follows individually:

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