Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL

DOI10.1007/978-3-540-74621-8_1zbMath1148.68466OpenAlexW1807554065MaRDI QIDQ3524998

Amit Goel, Sava Krstić

Publication date: 16 September 2008

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74621-8_1

Mathematics Subject Classification ID

Related Items (16)

A proof system for graph (non)-isomorphism verification ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Formalization and implementation of modern SAT solvers ⋮ Satisfiability Modulo Theories ⋮ Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Constraint solving for finite model finding in SMT solvers ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ Ground Interpolation for Combined Theories ⋮ Unnamed Item ⋮ Cutting to the Chase Solving Linear Integer Arithmetic ⋮ Conflict-driven satisfiability for theory combination: transition system and completeness ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Theory decision by decomposition

Uses Software

• MiniSat
• Yices
• Chaff

This page was built for publication: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL