Please use this identifier to cite or link to this item: https://research.matf.bg.ac.rs/handle/123456789/594
Title: Formalization and implementation of modern SAT solvers
Authors: Marić, Filip 
Affiliations: Informatics and Computer Science 
Keywords: Algorithms;Data structures;DPLL;SAT solving;Software verification
Issue Date: 1-Jun-2009
Journal: Journal of Automated Reasoning
Abstract: 
Most, if not all, state-of-the-art complete SAT solvers are complex variations of the DPLL procedure described in the early 1960's. Published descriptions of these modern algorithms and related data structures are given either as high-level state transition systems or, informally, as (pseudo) programming language code. The former, although often accompanied with (informal) correctness proofs, are usually very abstract and do not specify many details crucial for efficient implementation. The latter usually do not involve any correctness argument and the given code is often hard to understand and modify. This paper aims to bridge this gap by presenting SAT solving algorithms that are formally proved correct and also contain information required for efficient implementation. We use a tutorial, top-down, approach and develop a SAT solver, starting from a simple design that is subsequently extended, step-by-step, with a requisite series of features. The heuristic parts of the solver are abstracted away, since they usually do not affect solver correctness (although they are very important for efficiency). All algorithms are given in pseudo-code and are accompanied with correctness conditions, given in Hoare logic style. The correctness proofs are formalized within the Isabelle theorem proving system and are available in the extended version of this paper. The given pseudo-code served as a basis for our SAT solver argo-sat. © 2009 Springer Science+Business Media B.V.
URI: https://research.matf.bg.ac.rs/handle/123456789/594
ISSN: 01687433
DOI: 10.1007/s10817-009-9127-8
Appears in Collections:Research outputs

Show full item record

SCOPUSTM   
Citations

34
checked on Dec 19, 2024

Page view(s)

22
checked on Dec 23, 2024

Google ScholarTM

Check

Altmetric

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.