[red_admiral]

> If there are two algorithms that satisfy the same requirements, and only one is NP-complete, you pick the other one.

Problems can be NP-complete. Algorithms cannot - they can be exponential time (and if your choice is between exponential and double exponential, you pick the former!)

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. In some more academic cases, we even have heuristic solvers that are not even guaranteed to terminate, but usually do so within a couple of seconds, so you can get away with the "beginner's solution to the halting problem".

[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.