|
|
|
|
|
by svat
1213 days ago
|
|
My vague impression is that BDDs are good for the kinds of problems Knuth is interested in: exact answers, exhaustive enumeration, naive backtracking would be too slow, etc. So things like "there are exactly 13,267,364,410,532 undirected closed knight's tours on an 8x8 board". For those, BDDs can be much more efficient than writing out a giant truth table (so they're an amazing trick that can make certain things feasible to program that wouldn't otherwise be, and you can see why he likes them), but they hit their limits: the catch is that they are useful precisely when your Boolean function of interest has a small BDD, and not all functions will. In some sense, optimization algorithms (for traveling salesman, integer linear programming…) are all about avoiding exhaustive enumeration with lots of tricks like branch-and-bound etc, so BDDs are not very useful there (AFAIK). The examples mentioned on Wikipedia (circuits, formal verification) are ones where exhaustive enumeration is desired and you really want to examine every case, which is not true for the bulk of SAT solver applications / other NP-complete optimization problems. |
|