Extracting a DPLL Algorithm

Photograph of Andy Lawrence

Andy Lawrence


We formalize a completeness proof for the DPLL proof system and extract a DPLL solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a derivation which shows that it is unsatisfiable. We use non-computational quantifiers to remove redundant computational content from the program and improve its performance. The formalization is carried out in the Minlog system.
Thursday 10th May 2012, 14:00
Board Room
Department of Computer Science