[taeric]

Agreed with all of that. I would add BDDs and such in there, as great breakthroughs. In a very real sense, they are essentially moving how the computer builds up logical circuits into a data structure. (That is, I'm asserting that the math unit on a computer is closer to a BDD than it is any other data structure in computer science.)

But, even outside of advanced modeling, I'm always amazed at how much effort we go through to not reduce our problems to the computation that we want them to be. Instead of seeing our programs as tools to translate from a high level model to a low level one, we seem to want that low level model to be completely implicit and not visible in what we build.

Even code I have seen that uses solvers, there is rarely a good separation of "convert this problem specification into a SAT problem" with a corresponding "convert this SAT solution into the problem specification."

I /think/ this is where programs that do focus on text seem to have a win. You have a "how to convert this text to a SAT problem", "how to convert this text to a problem specification", and "how to convert this solution to a problem specification." Stabilize what those text representations are, and you get to spend a ton of effort at each section without immediate impact on the other areas.

[dc443]

Could you give some examples of how BDDs are impactful?

[taeric]

Sadly, I am mainly going on the praise I've seen from Knuth and similar. Use in CAD for circuits is what wikipedia has to say, but doesn't really give any links.

As such, mayhap I am misattributing how impactful they are?

[svat]

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.

[taeric]

Fair. I had fun playing with a basic BDD to "solve" a linear boolean program at https://taeric.github.io/trading-with-bdds.html. That said, I know that is a toy usage of the data structure, as such I don't have any other data there. I /thought/ I had seen more examples of where it was a good data structure, but I can't find those offhand. :(