The DPLL procedure has found great success in SAT, where search terminates on the first solution discovered. We show that this procedure is equally promising in a problem where exhaustive search is used, given that it is augmented with appropriate caching. Specifically, we describe a DPLL-based algorithm that constructs OBDDs for CNF formulas, and show how modern SAT techniques can be harnessed by implementing the algorithm directly on top of an existing SAT solver. We discuss the advantage of this new construction method over the traditional approach, where OBDDs for subsets of the CNF formula are built and conjoined. Our experiments indicate that on many standard benchmarks, the new method runs orders of magnitude faster than a comparable implementation of the traditional method. We also describe, on the other hand, a general class of CNFs where we have evidence that the traditional approach may be preferable.