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.

• Type: Conference
• Year: 1994
• Where: CCL
• Authors: Tomás E. Uribe, Mark E. Stickel
• Keywords: Automated Reasoning, Binary Decision Diagrams, CCL 1994, Functional Equivalence Problems, Prominent Decision Procedures