Formalization and implementation of modern SAT solvers

DOI10.1007/S10817-009-9127-8MaRDI QIDQ839035zbMATH OpenOpenAlexFDO

Authors Filip Marić

Publication date 1 September 2009

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

Full work available at URL https://doi.org/10.1007/s10817-009-9127-8

zbMATH Keywords

algorithmsdata structuresSAT solvingsoftware verificationDPLL

Mathematics Subject Classification ID

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

Recommendations

• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalization of Abstract State Transition Systems for SAT
• scientific article; zbMATH DE number 5605058
• Present and Future of Practical SAT Solving
• scientific article; zbMATH DE number 5713654

Cites work

• scientific article; zbMATH DE number 1951639 (Why is no real title available?)
• scientific article; zbMATH DE number 2080328 (Why is no real title available?)
• scientific article; zbMATH DE number 1903342 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An axiomatic basis for computer programming
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• Isabelle/HOL. A proof assistant for higher-order logic
• The complexity of theorem-proving procedures

Cited in

(18)

• scientific article; zbMATH DE number 2165692 (Why is no real title available?)
• A verified SAT solver framework with learn, forget, restart, and incrementality
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Practical algorithms for unsatisfiability proof and core generation in SAT solvers
• Formalization of Abstract State Transition Systems for SAT
• Efficient, verified checking of propositional proofs
• An expressive model for instance decomposition based parallel SAT solvers
• Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
• versat: A Verified Modern SAT Solver
• URBiVA: uniform reduction to bit-vector arithmetic
• The mechanical verification of a DPLL-based satisfiability solver
• SAT-Based Formula Simplification
• Formally verified tableau-based reasoners for a description logic
• Formalized proof systems for propositional logic
• Verifying the conversion into CNF in dafny
• scientific article; zbMATH DE number 7199588 (Why is no real title available?)
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Verified AIG algorithms in ACL2

Describes a project that uses

Uses Software

• MiniSat
• SATO
• Chaff
• BerkMin
• PicoSAT
• Archive Formal Proofs
• SAT Solver Verification

This page was built for publication: Formalization and implementation of modern SAT solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q839035)