Filip Maric ; Predrag Janicic - Formalization of Abstract State Transition Systems for SAT

lmcs:843 - Logical Methods in Computer Science, September 28, 2011, Volume 7, Issue 3 -
Formalization of Abstract State Transition Systems for SATArticle

Authors: Filip Maric ; Predrag Janicic

    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.

    Volume: Volume 7, Issue 3
    Published on: September 28, 2011
    Imported on: December 7, 2010
    Keywords: Computer Science - Logic in Computer Science,F.3.1, F.4.1
      Source : OpenAIRE Graph
    • Automated Reasoning and Data Mining; Funder: Ministry of Education, Science and Technological Development of Republic of Serbia; Code: 174021
    • Decision Procedures: from Formalizations to Applications; Funder: Swiss National Science Foundation; Code: 127979

    7 Documents citing this article

    Consultation statistics

    This page has been seen 1186 times.
    This article's PDF has been downloaded 284 times.