Idea of Quantifier-Free Combination

We know of several classes of formulas that we can decide:

ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols) - congruence closure
- $f(f(f(f(a)))) \neq a \land f(f(a))=a$
term algebras (interpreted over Herbrand model) - unification
- $cons(a,b)=cons(c,d) \land a \neq c$
real linear arithmetic - linear programming such as Simplex
- $x < y \land y < x + 1$
integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT
- $x < y \land y < x + 1$

We wish to reason about quantifier-free formulas that contain all these different symbols in the same formula.

The idea is to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately.

We are checking satisfiability. $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable.

$\begin{equation*} F \ \ \leftrightarrow \ \ \bigvee_{i=1}^n C_i \end{equation*}$

We therefore consider conjunctions of literals $C_i$ .

Consider a conjunction of literals $C$ . If we can group literals into blocks

$\begin{equation*} C \leftrightarrow C_1 \land \ldots \land C_n \end{equation*}$

If one of the $C_i$ is unsatisfiable, then $C$ is unsatisfiable.

The idea is to separate conjuncts into those specific to individual theories, and then solve each $C_i$ using a specialized decision procedure $P_i$

An important question is completeness: if each $C_i$ is satisfiable, is $C_1 \land \ldots \land C_n$ satisfiable? We will show that, under certain conditions, this holds.