Satisfiability modulo theories and assignments

Abstract

The 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ć. Furthermore, CDSAT generalizes the equality sharing (Nelson-Oppen) approach to theory combination, by allowing theories to share equality information both explicitly through equalities and disequalities, and implicitly through assignments. We identify sufficient conditions for the soundness, completeness, and termination of CDSAT.