Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness

Many applications depend on solving the satisfiability of formulæ involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory. This article presents a new method for satisfiability modulo a combination of theories, named CDSAT, for Conflict-Driven SATisfiability . CDSAT also solves Satisfiability Modulo Assignment problems that may include assignments to first-order terms. A conflict-driven procedure assigns values to variables to build a model, and performs inferences on demand in order to solve conflicts between assignments and formulæ. CDSAT extends this paradigm to generic combinations of disjoint theories, each characterized by a collection of inference rules called theory module . CDSAT coordinates the theory modules in such a way that the conflict-driven reasoning happens in the union of the theories , not only in propositional logic. As there is no fixed hierarchy with propositional logic at the center and the other theories as satellites, CDSAT offers a flexible framework for model search. We prove the soundness , completeness , and termination of CDSAT, identifying sufficient requirements on theories and modules that ensure these properties.