Sciweavers

Share
CCL
1994
Springer

Ordered Binary Decision Diagrams and the Davis-Putnam Procedure

11 years 9 months ago
Ordered Binary Decision Diagrams and the Davis-Putnam Procedure
Abstract. We compare two prominent decision procedures for propositional logic: Ordered Binary Decision Diagrams (obdds) and the DavisPutnam procedure. Experimental results indicate that the Davis-Putnam procedure outperforms obdds in hard constraint-satisfaction problems, while obdds are clearly superior for Boolean functional equivalence problems from the circuit domain, and, in general, problems that require the schematization of a large number of solutions that share a common structure. The two methods illustrate the di erent and often complementary strengths of constraint-oriented and search-oriented procedures.
Tomás E. Uribe, Mark E. Stickel
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where CCL
Authors Tomás E. Uribe, Mark E. Stickel
Comments (0)
books