@inproceedings{e39f9a28c7264e7c986ad955127a740e,
title = "Extended Resolution Proofs for Conjoining BDDs.",
abstract = "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 insteador in combination withestablished 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.",
author = "Carsten Sinz and Armin Biere",
year = "2006",
doi = "10.1007/11753728\_60",
language = "English",
isbn = "978-3-540-34166-6",
volume = "3967",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "600--611",
booktitle = "Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006)",
}