The Mechanical Verification of a DPLL-Based Satisfiability Solver
From MaRDI portal
Publication:5179007
DOI10.1016/j.entcs.2011.03.002zbMath1347.68307OpenAlexW2080046595WikidataQ113318278 ScholiaQ113318278MaRDI QIDQ5179007
Natarajan Shankar, Marc Vaucher
Publication date: 18 March 2015
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2011.03.002
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
versat: A Verified Modern SAT Solver ⋮ Verifying the conversion into CNF in dafny ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Efficient, verified checking of propositional proofs ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Unnamed Item ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ Formally verified tableau-based reasoners for a description logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formalization and implementation of modern SAT solvers
- Towards mechanical metamathematics
- Simplify: a theorem prover for program checking
- Graph-Based Algorithms for Boolean Function Manipulation
- A mechanical proof of the Church-Rosser theorem
- Metamathematics, Machines and Gödel's Proof
- GRASP: a search algorithm for propositional satisfiability
- SATO: An efficient propositional prover
- A Tutorial on Satisfiability Modulo Theories
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
This page was built for publication: The Mechanical Verification of a DPLL-Based Satisfiability Solver
