Carsten Sinz, Armin Biere,
"Extended Resolution Proofs for Conjoining BDDs."
: Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006), Serie Lecture Notes in Computer Science (LNCS), Vol. 3967, Springer Verlag, Seite(n) 600-611, 2006, ISBN: 978-3-540-34166-6
Original Titel:
Extended Resolution Proofs for Conjoining BDDs.
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 1st Intl. Computer Science Symp. in Russia (CSR 2006)
Original Kurzfassung:
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.
Forschungs-