Satisfiability Modulo Theories and Assignments

Maria Paola Bonacina (1) , Stéphane Graham-Lengrand (2, 3, 4, 5) , Natarajan Shankar (3)

1 UNIVR - Università degli studi di Verona = University of Verona
2 CNRS - Centre National de la Recherche Scientifique
3 SRI - SRI International [Menlo Park]
4 PARSIFAL - Proof search and reasoning with logic specifications
5 X - École polytechnique

The CDCL procedure for SAT is the archetype of conflict-driven procedures for satisfiability of quantifier-free problems in a single theory. In this paper we lift CDCL to CDSAT (Conflict-Driven Satisfia-bility), a system for conflict-driven reasoning in combinations of disjoint theories. CDSAT combines theory modules that interact through a global trail representing a candidate model by Boolean and first-order assignments. CDSAT generalizes to generic theory combinations the model-constructing satisfiability calculus (MCSAT) introduced by de Moura and Jovanovi´cJovanovi´c. Furthermore, CDSAT generalizes the equality sharing (Nelson-Oppen) approach to theory combination, by allowing theories to share equality information both explicitly through equalities and dis-equalities, and implicitly through assignments. We identify sufficient conditions for the soundness, completeness, and termination of CDSAT.

Mots clés: Theory combination; Conflict-driven decision procedures; Model building; Satisfiability modulo assignment

Domaines: Logique en informatique [cs.LO]

Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. Satisfiability Modulo Theories and Assignments. CADE 2017 - 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. ⟨10.1007/978-3-319-63046-5_4⟩. ⟨hal-01615830⟩