I'm continually confused why SAT solving is seen as a bad thing. It automatically solves common real-world problems in less than a second even in absurdly extreme cases, and a couple milliseconds normally - why would you avoid it?
Go's algorithm is much simpler and does not need a lockfile while still giving deterministic results. Ranged deps without a lockfile cannot. There is benefit to two people running the same command and getting the same dependency versions. Most projects do not start with a lockfile, so it is quite easy to have different versions when running getting started commands.
Another example, if I install two ranged dependencies in both orders, will I get the same final deps@version list?