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) - congruence closure
- term algebras (interpreted over Herbrand model) - unification
- real linear arithmetic - linear programming such as Simplex
- integer linear arithmetic - integer linear programming (branch and bound, branch and cut), reduction to SAT
We would like to separate a quantifier-free formula into constraints that talk only about individual theories, and solve each constraint separately.
We are checking satisfiability. is satisfiable iff each disjunct in its disjunctive normal form is satisfiable. We therefore consider conjunctions of literals.
Consider a conjunction of literals . If we can group literals into blocks, and
- if one of the is unsatisfiable, then is unsatisfiable
The idea is to separate conjuncts into those specific to individual theories, and then solve each using a specialized decision procedure
An important question is completeness: if each is satisfiable, is satisfiable? We will show that, under certain conditions, this holds.