CDSAT: conflict-driven satisfiability modulo theories and assignments

The success of Conflict-Driven Clause Learning (CDCL) for propositional satisfiability motivates the quest for methods that realize the principle of conflict-driven reasoning for richer logics. After generalizing CDCL to first-order logic with SGGS, I worked on CDSAT, that generalizes CDCL to satisfiability in combinations of theories and satisfiability modulo assignments:

CDCL, SGGS, and CDSAT are instances of a paradigm of conflict-driven reasoning:

Maria Paola Bonacina