The CDSAT method for satisfiability modulo theories and assignment: an exposition

DOI10.1007/978-3-031-95908-0_1MaRDI QIDQ6897667zbMATH OpenFDO

Authors Maria Paola Bonacina

Publication date 19 November 2025

Full work available at URL https://doi.org/10.1007/978-3-031-95908-0_1

zbMATH Keywords

combination of theoriesconflict-driven satisfiability proceduressatisfiability modulo theory and assignment

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A model-constructing satisfiability calculus
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• Conflict-driven satisfiability for theory combination: transition system and completeness
• Cutting to the chase.
• Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
• DPLL: the core of modern satisfiability solvers
• Generalizing DPLL to Richer Logics
• GRASP: a search algorithm for propositional satisfiability
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 5194318 (Why is no real title available?)
• Model-based theory combination
• On Fourier's algorithm for linear arithmetic constraints
• Simplification by Cooperating Decision Procedures
• Solving non-linear arithmetic
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Splitting on Demand in SAT Modulo Theories
• Theory combination: beyond equality sharing

This page was built for publication: The CDSAT method for satisfiability modulo theories and assignment: an exposition

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6897667)