BDDs are a way of representing Boolean formulas.
DPLL is an algorithm to determine satisfiability of Boolean formulas.
My understanding is that the two are used for SAT solving.
How are they combined?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
They're not combined. They are two separate techniques.
DPLL is used with a Boolean formula represented in CNF form. BDD algorithms represent the Boolean formula as a BDD.
Generally, if you want to test satisfiability, DPLL-based SAT solvers are likely to be more effective. BDDs do allow performing other operations that go beyond satisfiability, which might be useful in some settings.
As a rough rule of thumb, BDDs are older technology and SAT solvers are newer technology, and for many tasks we're trying to automate, solutions that build on SAT solvers tend to outperform solutions that build on BDDs. But it all depends on the specific problem you're dealing with, and there are no hard-and-fast rules.
