Conflict-driven satisfiability for theory combination: transition system and completeness

DOI10.1007/s10817-018-09510-yzbMath1468.68194OpenAlexW2907207368MaRDI QIDQ2303254

Natarajan Shankar, Maria Paola Bonacina, Stéphane Graham-Lengrand

Publication date: 3 March 2020

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-018-09510-y

zbMATH Keywords

model buildingtheory combinationsatisfiability modulo assignmentconflict-driven decision procedures

Mathematics Subject Classification ID

Logic in computer science (03B70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (6)

Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Solving bitvectors with MCSAT: explanations from bits and pieces ⋮ SGGS decision procedures

Uses Software

• Yices

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Satisfiability modulo theories and assignments
• Deciding Bit-Vector Formulas with mcSAT
• Solving Non-linear Arithmetic
• A Model-Constructing Satisfiability Calculus
• Solving Nonlinear Integer Arithmetic with MCSAT
• Sharing Is Caring: Combination of Theories
• Solving SAT and SAT Modulo Theories
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Simplification by Cooperating Decision Procedures
• Cutting to the Chase Solving Linear Integer Arithmetic
• Splitting on Demand in SAT Modulo Theories

This page was built for publication: Conflict-driven satisfiability for theory combination: transition system and completeness