Satisfiability Modulo Theories and Assignments

International audienceThe CDCL procedure for SAT is the archetype of conflict-driven procedures for satisfiability of quantifier-free problems in a single theory. In this paper we lift CDCL to CDSAT (Conflict-Driven Satisfia-bility), a system for conflict-driven reasoning in combinations of disjoint theories. CDSAT combines theory modules that interact through a global trail representing a candidate model by Boolean and first-order assignments. CDSAT generalizes to generic theory combinations the model-constructing satisfiability calculus (MCSAT) introduced by de Moura and Jovanovi´cJovanovi´c. Furthermore, CDSAT generalizes the equality sharing (Nelson-Oppen) approach to theory combination, by allowing theories to share equality information both explicitly through equalities and dis-equalities, and implicitly through assignments. We identify sufficient conditions for the soundness, completeness, and termination of CDSAT