Yes, Cargo doesn't use a SAT solver, but Cargo' source code acknowledges that "solving a constraint graph is an NP-hard problem" and uses "nice heuristic to make sure we get roughly the best answer most of the time". [1]
It's not just a theoretical consideration. It can create real problems. See for example "Abort crate resolution if too many candidates have been tried" at https://github.com/rust-lang/cargo/issues/4066. I'm not saying it's big issue, but it's something to consider in the design space and this is why the Go team is considering other options.
[1] https://github.com/rust-lang/cargo/blob/master/src/cargo/cor...
I respect Russ Cox's decision to favor different considerations for Go's versioning story. The approach of constraining to minimal versions is not bad, merely different (especially since the -u flag exists). But the framing of this as solving some problem with existing package managers is simply mistaken, as Russ would know if he had used these tools in practice, rather than instinctively reeling at the theoretical implications.
It's not fair to accuse people of not doing their homework when they actually are...
Russ Cox published "Version SAT" in December 2016. [1] The article specifically mentions "Rust's Cargo" which "uses a basic backtracking solver".