Formalization and implementation of modern SAT solvers

DOI10.1007/s10817-009-9127-8zbMath1187.68557OpenAlexW2021196646MaRDI QIDQ839035

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 structuressoftware verificationSAT solvingDPLL

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 (11)

The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Verifying the conversion into CNF in dafny ⋮ Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL ⋮ Efficient, verified checking of propositional proofs ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ Unnamed Item ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ The Mechanical Verification of a DPLL-Based Satisfiability Solver ⋮ URBiVA: Uniform Reduction to Bit-Vector Arithmetic ⋮ Unnamed Item ⋮ Formally verified tableau-based reasoners for a description logic

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
• An axiomatic basis for computer programming
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures

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