2 ms·
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
by abecedarius 6y ago
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).
- UncleMeat 6y ago> 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.