We compare two prominent decision procedures for propositional logic: Ordered Binary Decision Diagrams (Obdds) and the Davis-Putnam 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 different and often complementary strengths of constraint-oriented and search-oriented procedures.