Conflict-driven satisfiability for theory combination: transition system and completeness

Many applications depend on solving the satisfiability of formulae involving propositional logic and first-order theories, a problem known as Satisfiability Modulo Theory (SMT). 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 (SMA) 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 formulae. 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.