List DILS invites you to their event
About this event
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 its variants, and MCSAT.
(CDSAT is joint work with Stéphane Graham-Lengrand and Natarajan Shankar.)
Le CEA est un organisme de recherche sur la défense et la sécurité, les énergies nucléaire et renouvelables, la recherche technologique pour l’industrie et la recherche fondamentale en sciences de la matière et de la vie.
