< Retour au sommaire

The CDSAT Paradigm for Theory Combination in SMT

Maria Paola Bonacina le

Lieu: Amphi 33

Suivre en visio

Abstract

Most SMT instances involve symbols from more than one theory. The Nelson-Oppen scheme for combining theory satisfiability procedures has been a standard for over forty years. For the Boolean part, Nelson-Oppen is interfaced with the CDCL (Conflict-Driven Clause Learning) procedure for SAT. CDCL guides the search by learning lemmas from conflicts between clauses and candidate model. In the resulting CDCL(T) integration the conflict-driven reasoning remains propositional. Theory procedures where the conflict-driven reasoning is first-order do exist, but neither Nelson-Oppen nor CDCL(T) accommodate them. MCSAT (Model-Constructing SATisfiability) integrates CDCL with a single conflict-driven theory procedure, but MCSAT is not a theory combination calculus. CDSAT (Conflict-Driven SATisfiability) generalizes MCSAT to theory combination by integrating multiple (conflict-driven or not) theory procedures, including CDCL. In CDSAT the reasoning in the theory union is conflict-driven. This talk gives an exposition of CDSAT, applying it to examples of increasing expressivity and showing how it generalizes CDCL, CDCL(T), Nelson-Oppen and i s variants, and MCSAT.

(CDSAT is joint work with Stéphane Graham-Lengrand and Natarajan Shankar.)