2012•Electronic Notes in Theoretical Computer ScienceOpen access
Extracting a DPLL Algorithm
Andrew D. Lawrence, Ulrich Berger, Monika Seisenberger
Open full text 2 citations
Abstract
We formalize a completeness proof for the DPLL proof system and extract a DPLL SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation which shows that it is unsatisfiable. We use non-computational quantifiers to remove redundant computational content from the extracted program and improve its performance. The formalization is carried out in the Minlog system.
Open-access reader