Difference of BDD and SAT(CNF)

An Integrated Approach for Combining BDDs and SAT Provers,
by Rolf Drechsler, Gorschwin Fey, and Sebastian Kinder
FACTA UNIVERSITATIS (NIS)ˇSER.: ELEC. ENERG. vol. 20. no. 3, December 2007, 415-436

The two most frequently used methods are Binary Decision Diagrams (BDDs) and provers for Boolean Satisfiability (SAT). Experimental studies have shown that these techniques are orthogonal, i.e. there exist problems where BDDs work well, while SAT solvers fail and vice versa. This trade-off can even be formally proven [4].

BDDs and SAT provers are very different in nature. While BDDs compute all solutions in parallel, they require a large amount of memory. In contrast SAT is very efficient regarding memory consumption, but only gives a single solution. There are many applications where multiple solutions are needed (see e.g. [5, 6]). Motivated by this, many authors tried to combine the best of the two approaches, by applying SAT solvers and BDDs alternatively or iteratively. Even though remarkable results have been obtained, so far none of the approaches considered an integration of the
two methods within a single data structure. (A more detailed discussion of related work is given in the next section.)