Formalization of Abstract State Transition Systems for SAT

DOI10.2168/LMCS-7(3:19)2011MaRDI QIDQ3224685zbMATH OpenOpenAlexFDO

Authors Filip Marić, Predrag Janičić

Publication date 2 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1108.4368

zbMATH Keywords

abstract state transition systemsformal verificationIsabelle/HOLSAT solving

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We present a formalization of modern SAT solvers and their properties in a form of abstract state transition systems. SAT solving procedures are described as transition relations over states that represent the values of the solver's global variables. Several different SAT solvers are formalized, including both the classical DPLL procedure and its state-of-the-art successors. The formalization is made within the Isabelle/HOL system and the total correctness (soundness, termination, completeness) is shown for each presented system (with respect to a simple notion of satisfiability that can be manually checked). The systems are defined in a general way and cover procedures used in a wide range of modern SAT solvers. Our formalization builds up on the previous work on state transition systems for SAT, but it gives machine-verifiable proofs, somewhat more general specifications, and weaker assumptions that ensure the key correctness properties. The presented proofs of formal correctness of the transition systems can be used as a key building block in proving correctness of SAT solvers by using other verification approaches.

Recommendations

• Formalization and implementation of modern SAT solvers
• Systematic Refinement of Abstract State Machines with Higher-Order Logic
• Formal verification of a generic framework to synthesize SAT-provers
• SAT-Based Model Checking
• scientific article; zbMATH DE number 2102724
• scientific article; zbMATH DE number 1759636
• scientific article; zbMATH DE number 1841822

Cited in

(9)

• A verified SAT solver framework with learn, forget, restart, and incrementality
• Verifying the conversion into CNF in dafny
• Functional encryption for inner product with full function privacy
• scientific article; zbMATH DE number 1324665 (Why is no real title available?)
• A proof system for graph (non)-isomorphism verification
• Verified verifying: SMT-LIB for strings in Isabelle
• On enumerating short projected models
• Certainty in formalising SMT-LIB for strings in Isabelle
• Formalization and implementation of modern SAT solvers

Describes a project that uses

Uses Software

• BerkMin
• seL4
• Chaff
• MiniSat
• SAT Solver Verification
• Archive of Formal Proofs
• Isabelle/HOL
• PicoSAT
• SATO

This page was built for publication: Formalization of Abstract State Transition Systems for SAT

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