Satisfiability modulo theories and assignments

We present an abstract framework for solving satisfiability problems in quantifier-free first-order logic modulo a combination of disjoint theories. Our framework combines theory modules interacting through a trail representing a candidate model by Boolean and first-order assignments. We define a semantic, assignment-carrying, inference system, named CDSAT for Conflict-Driven Satisfiability, that generalizes to generic theory combinations the model-constructing satisfiability calculus (MCSAT) introduced by de Moura and Jovanovic. We identify requirements for theories and theory modules from which we prove soundness, completeness, and termination of CDSAT. Furthermore, CDSAT generalizes the Nelson-Oppen approach to theory combination by allowing theories to share equality information both explicitly through equalities and disequalities, and implicitly through model construction.