SAT Solver Verification

MaRDI QIDQ40545swMATHFDO

Authors Filip Marić

Publication date 23 July 2008

Official website https://www.isa-afp.org/entries/SATSolverVerification.html

Cites work

• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)

Described by source

• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

Cited in

(11)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• versat
• A verified SAT solver framework with learn, forget, restart, and incrementality
• IsaFoL
• Formalization of Abstract State Transition Systems for SAT
• DPT
• Completeness theorem
• Paraconsistency
• Propositional Resolution
• Epistemic Logic
• Formalization and implementation of modern SAT solvers

This page was built for software: SAT Solver Verification