Cooperation of Decision Procedures for the Satisfiability Problem

Abstract : Constraint programming is strongly based on the use of solvers which are able to check satisfiability of constraints. We show in this paper a rule-based algorithm for solving in a modular way the satisfiability problem w.r.t. a class of theories $Th$. The case where $Th$ is the union of two disjoint theories $Th_1$ and $Th_2$ is known for a long time but we study here different cases where function symbols are shared by $Th_1$ and $Th_2$. The chosen approach leads to a highly non-deterministic decomposition algorithm but drastically simplifies the understanding of the combination problem. The obtained decomposition algorithm is illustrated by the combination of non-disjoint equational theories.