Extracting a DPLL Algorithm | Zendy

Andrew D. Lawrence | Zendy; Ulrich Berger | Zendy; Monika Seisenberger | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Extracting a DPLL Algorithm

Author(s) -

Andrew D. Lawrence,

Ulrich Berger,

Monika Seisenberger

Publication year - 2012

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2012.08.016

Subject(s) - dpll algorithm , completeness (order theory) , conjunctive normal form , computer science , algorithm , solver , boolean satisfiability problem , disjunctive normal form , theoretical computer science , mathematics , programming language , phase locked loop , mathematical analysis , telecommunications , jitter

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research