This is an old revision of the document!

Idea of Quantifier-Free Combination

We wish to reason about quantifier-free formulas that contain different symbols, such as

ground formulas interpreted over arbitrary functions and relations (also called uninterpreted function symbols)
term algebras (interpreted over Herbrand model)
integer linear arithmetic
real linear arithmetic

For this, we would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately.

Note that we are checking satisfiability, and $F$ is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. We therefore consider conjunctions of literals.

Consider a conjunction of literlas $C$ . If we can represent it as separate conjunction $C_1$ ,…, $C_n$ then

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.