[surrealize]

There was some discussion about potentially using a SAT solver for cargo in this issue:

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