[munificent]

> In practice, and especially for SAT solving, as far as I understand the state of the art is that the general case is NP-hard but we have tools that work surprisingly well in those cases that reality tends to produce.

You're correct. Modern version solvers need fairly sophisticated algorithms, but it's not rocket science. It's mostly a non-problem for most users of most package managers most of the time.

[bennofs]

The thing that worries me about this line of thinking is that as far as I know, we don't know much about why SAT solvers tend to work well in practice. So if I ever happen to hit a problem that the solver cannot solve, all we can say is "well bad luck". If the algorithm fails, I won't have any way to know why. This strikes me as a bad situation to be in.