Extended Resolution Proofs for Conjoining BDDs

We present a method to convert the construction of binary decision diagrams (BDDs) into extended resolution proofs. Besides in proof checking, proofs are fundamental to many applications and our results allow the use of BDDs instead--or in combination with--established proof generation techniques, based for instance on clause learning. We have implemented a proof generator for propositional logic formulae in conjunctive normal form, called EBDDRES. We present details of our implementation and also report on experimental results. To our knowledge this is the first step towards a practical application of extended resolution.

• Type: Conference
• Year: 2006
• Where: CSR
• Authors: Carsten Sinz, Armin Biere
• Keywords: Binary Decision Diagrams, CSR 2006, Proof Generation Techniques, Propositional Logic Formulae, Theoretical Computer Science