There was some discussion about potentially using a SAT solver for cargo in this issue: https://github.com/rust-lang/cargo/issues/2064 https://github.com/rust-

There was some discussion about potentially using a SAT solver for cargo in this issue: https://github.com/rust-lang/cargo/issues/2064 https://github.com/rust-lang/cargo/issues/2064 and graydon wrote a POC of using the Z3 solver to find a solution where semver constraints were satisfied, optimizing for the latest versions within those constraints: https://github.com/graydon/z3-rs/blob/master/tests/semver_tests.rs#L158-L267 https://github.com/graydon/z3-rs/blob/master/tests/semver_te...