The CDSAT method for satisfiability modulo theories and assignments: an exposition

Most SMT instances involve symbols from more than one theory. The equality sharing method for combining theory satisfiability procedures has been a standard for over forty years. For the Boolean part, the equality sharing method is interfaced with the CDCL procedure for SAT. CDCL guides the search by learning lemmas from conflicts between clauses and candidate model. In the standard integration of CDCL and equality sharing, the conflict-driven reasoning remains propositional, even if conflict-driven theory procedures exist. The MCSAT method integrates CDCL with a single conflict-driven theory procedure. The CDSAT method generalizes CDCL, MCSAT, and equality sharing, by allowing the integration of multiple (conflict-driven or not) theory procedures.