BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem. A SAT solver might not be as predictable (though I don't have the experience to say how big this issue is in practice).
A BDD can also efficiently answer questions like "how many ways can you satisfy this formula?" (subject to the same caveat about problem suitability).
> BDDs are simple and predictable provided you know that the variable ordering that you're using will compactly encode your problem.
Sadly, variable ordering is NP-Hard. This is brutal for static analysis applications where BDDs seem like they are going to save the world but often end up crushing dreams.
A BDD can also efficiently answer questions like "how many ways can you satisfy this formula?" (subject to the same caveat about problem suitability).