The Mechanical Verification of a DPLL-Based Satisfiability Solver

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

zbMATH Keywords

SAT solverPVSdependent typebacklumpingpredicate subtype

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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

• PVS
• Yices
• SATO
• SIMPLIFY
• Chaff

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