CDSAT and QSMA for satisfiability modulo theories and assignments

The success of Conflict-Driven Clause Learning (CDCL) for propositional satisfiability motivated the quest for methods that do conflict-driven reasoning in more expressive logics. After generalizing CDCL to first-order logic with SGGS, I worked on the CDSAT (conflict-driven satisfiability) method, which generalizes CDCL, CDCL(T), MCSAT, and the Nelson-Oppen scheme, to achieve conflict-driven reasoning in unions of theories modulo assignments. The current version of CDSAT is for quantifier-free problems. Thus, I also worked on the QSMA (quantified satisfiability modulo theories and assignments) algorithm, that decides the satisfiability of formulas with arbitrary quantification modulo a complete theory and an initial assignment. QSMA and CDSAT will be integrated in future work.

Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. CDSAT for predicate-sharing theories: arrays, maps, and vectors with abstract domain. Submitted to a journal, 45 pages (presented in part at the Workshop on Automated Reasoning and Proof Logging, Final EuroProofNet Symposium, Université Paris-Saclay, Paris, France, EU, September 2025: Slides and Video; and at the Workshop on Theory and Practice of SAT and Combinatorial Solving, Banff International Research Station for Mathematical Discovery and Innovation, Banff, Alberta, Canada, January 2026: Slides and Video).
Maria Paola Bonacina. The CDSAT method for satisfiability modulo theories and assignment: an exposition. In Proceedings of the 21st International Conference on Computability in Europe: Crossroads of Computability and Logic - Insights, Inspirations, and Innovations (CiE), Lisbon, Portugal, EU, July 2025. Springer, Lecture Notes in Computer Science 15764, 1-16, July 2025 (invited paper supporting an invited tutorial; presented also at CEA List, Paris, France, EU, October 2025: Slides); DOI: 10.1007/978-3-031-95908-0_1 (©[Springer Nature B.V.][2025]).
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. The QSMA algorithm for quantifiers in SMT. Journal of Automated Reasoning, 69(2):13, 40 pages, June 2025; DOI: 10.1007/s10817-025-09727-8; Springer Nature SharedIt (©[Springer Nature B.V.][2025]).
Maria Paola Bonacina. Reasoning about quantifiers in SMT: the QSMA algorithm (Abstract of keynote speech). In Proceedings of the 23rd International Conference on Formal Methods in Computer-Aided Design (FMCAD), Ames, Iowa, USA, October 2023. TU Wien Academic Press, 1-1, 2023; DOI: 10.34727/2023/isbn.978-3-85448-060-0_1.
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. QSMA: a new algorithm for quantified satisfiability modulo theory and assignment. In Proceedings of the 29th International Conference on Automated Deduction (CADE), Rome, Italy, EU, July 2023. Springer, Lecture Notes in Artificial Intelligence 14132, 78-95, 2023; DOI: 10.1007/978-3-031-38499-8_5 (presented at the Dagstuhl Seminar 23471 on The Next Generation of Deduction Systems: from Composition to Compositionality, November 2023: Slides).
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. CDSAT for nondisjoint theories with shared predicates: arrays with abstract length. In Proceedings of the 20th International Workshop on Satisfiability Modulo Theories (SMT) satellite of the 11th International Joint Conference on Automated Reasoning (IJCAR) held at the 8th Federated Logic Conference (FLoC), Haifa, Israel, August 2022. CEUR Volume 3185:18-37, 2022. (Presented at the Department of Computer Science of Yale University and at the Department of Computer Science of the University of Manchester: Slides)
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. Journal of Automated Reasoning 66(1):43-91, February 2022; DOI: 10.1007/s10817-021-09606-y; Springer Nature SharedIt (©[Springer Nature B.V.][2022]).
Maria Paola Bonacina. Proof generation in CDSAT. (Abstract of keynote speech) In Proceedings of the 7th International Workshop on Proof eXchange in Theorem Proving (PxTP), satellite of the 28th International Conference on Automated Deduction (CADE), Pittsburgh, Pennsylvania, USA, July 2021. Open Publishing Association, Electronic Proceedings in Theoretical Computer Science 336:1-4, 2021; DOI: 10.4204/EPTCS.336.1.
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Conflict-driven satisfiability for theory combination: transition system and completeness. Journal of Automated Reasoning, 64(3):579-609, March 2020; DOI: 10.1007/s10817-018-09510-y; Springer Nature SharedIt (©[Springer Nature B.V.][2020]).
Maria Paola Bonacina. Conflict-driven reasoning in unions of theories (Abstract of keynote speech). In Proceedings of the 12th International Symposium on Frontiers of Combining Systems (FroCoS), London, England, UK, September 2019. Springer, Lecture Notes in Artificial Intelligence 11715, xi-xiii, 2019 (Talk revised with title Conflict-Driven Satisfiability Modulo Assignments for the Seminar of the Theoretical Foundations of Computer Systems Program, Simons Institute for the Theory of Computing, Berkeley, California, USA, March 2021: Slides).
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Proofs in conflict-driven theory combination. In Proceedings of the 7th ACM International Conference on Certified Programs and Proofs (CPP) satellite of the 45th ACM Symposium on Principles of Programming Languages (POPL), Los Angeles, California, USA, January 2018. ACM Press, 186-200, 2018; DOI: 10.1145/3167096 (©[ACM Inc.][2018]) (archived in HAL as hal-01935595; the part on lemma learning was presented as a presentation-only talk at the 16th International Workshop on Satisfiability Modulo Theories (SMT), satellite of the 9th International Joint Conference on Automated Reasoning (IJCAR), held at the 7th Federated Logic Conference (FLoC), Oxford, England, UK, July 2018: Slides; the part on proof reconstruction was presented at the Dagstuhl Seminar 19371 on Deduction Beyond Satisfiability, September 2019).
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Natarajan Shankar. Satisfiability modulo theories and assignments. In Proceedings of the 26th International Conference on Automated Deduction (CADE), Gothenburg, Sweden, August 2017. Springer, Lecture Notes in Artificial Intelligence 10395, 42-59, 2017; DOI: 10.1007/978-3-319-63046-5_4 (presented at the Big Proof Program, Isaac Newton Institute for Mathematical Sciences, Cambridge, England, UK, July 2017: Slides and Video; an early version was presented in an invited talk at the 24th UK Automated Reasoning Workshop, The University of Bristol, Bristol, England, UK, April 2017: Slides).

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

Maria Paola Bonacina. On conflict-driven reasoning. In Proceedings of the 6th Workshop on Automated Formal Methods (AFM) satellite of the 9th NASA Formal Methods Symposium (NFM), Menlo Park, California, USA, May 2017. EasyChair Kalpa Publications in Computing 5, 31-49, April 2018; DOI: 10.29007/spwm.
Maria Paola Bonacina. Deduzione automatica. In Le Direzioni della Ricerca Logica in Italia - Volume 2. ETS Edizioni, Analitica, Chapter 3, 77-139, June 2018 (invited).

An implementation of CDSAT was explored in a prototype SMT/SMA solver named Eos written by Giulio Mazzi:

Maria Paola Bonacina and Giulio Mazzi. The Eos SMT/SMA-solver: a preliminary report. Presented at the 17th International Workshop on Satisfiability Modulo Theories (SMT), satellite of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT), 1-10, Lisbon, Portugal, EU, July 2019.

Maria Paola Bonacina