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 realize the principle of conflict-driven reasoning for richer logics. After generalizing CDCL to first-order logic with SGGS, I worked on the CDSAT (conflict-driven satisfiability) method, that generalizes CDCL, MCSAT, and the Nelson-Oppen scheme, to realize conflict-driven satisfiability 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 will be integrated in CDSAT 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. In preparation for submission to a journal, 46 pages.
Maria Paola Bonacina, Stéphane Graham-Lengrand, and Christophe Vauthier. The QSMA algorithm for quantifiers in SMT. Submitted to a journal, 44 pages.
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 Proceedings 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.
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.
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; 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