Add readme to resolver-tests crate

[ShuiRuTian]

Problem

It's surprised for me to find there is a SAT resolver in resolver-tests crate.

It looks strange,

• this resolver is not used anywhere
• rust allows install different versions of same package. But in my understanding, SAT only allows one version for each package.

So, it feels like it's useless? What is the purpose of this resolver? Another strategy which might be enabled in the future?

Steps

No response

Possible Solution(s)

No response

Notes

No response

Version

No response

[epage]

this resolver is not used anywhere

The SAT resolver is a re-implementation of our resolver for us to compare results against like with

cargo/crates/resolver-tests/src/lib.rs

Line 34 in e01eeb0

pub fn resolve_and_validated(

which is used in tests like

cargo/crates/resolver-tests/src/lib.rs

Line 34 in e01eeb0

pub fn resolve_and_validated(

But in my understanding, SAT only allows one version for each package.

I'm not one to be able to speak to those kind of details but the fact that the two resolvers match behavior means we've modeled it in SAT in a way that works.

[Eh2406]

@epage has summarize things pretty well, although he's pasted the same link twice. I am happy to answer any follow-up question you may have! The challenge will be getting me to stop talking. If you have specific questions feel free to ask them here, or come to my office hours. I would appreciate if you could turn your new understanding into documentation. @ShuiRuTian, when you are surprised to see this code, which documentation did you look at? Were there places you looked where there wasn't documentation? Were there confusing things about the documentation you did find?

Let's make (or move) answers to your questions, and put them where you would have found them!

[ShuiRuTian]

@Eh2406 Hi.

I read the comments in the file and some third-party documents:

• Version SAT, describe the SAT and package management: https://research.swtch.com/version-sat?ref=thefeedbackloop.xyz
• Thoughts on "Dependency hell is NP-complete", feels like the thought of a member of cargo: https://www.thefeedbackloop.xyz/thoughts-on-dependency-hell-is-np-complete

NOTE: here is some more docs, but not as important as the above ones

• pub solver, how dart's package manager works with SAT: https://github.com/dart-lang/pub/blob/master/doc/solver.md
• Simplifying the Solver with Functors: https://roscidus.com/blog/blog/2014/09/17/simplifying-the-solver-with-functors/

And I found most of SAT resolvers work for the environment that does not allow duplicated packages(.i.e, you could not have a package with different versions).

It feels like reasonable, if you could download different versions, SAT should be able to always give an answer, then it does not make much of sense to use SAT.

Finally, when I read the resolver of cargo, I wanted to have a look at test files firstly, then I am surprised to find cargo has a SAT resolver only for test. Especially the comment says "The SAT library dose not optimize for the newer version, so the selected packages may not match the real resolver."

Thanks for the following up!

[Eh2406]

I read the comments in the file

Looking around, you make a good point. We don't seem to have general documentation about what the resolver-tests crates are for. Would you be up for adding a reame.md to https://github.com/rust-lang/cargo/tree/master/crates/resolver-tests ?

pub solver, how dart's package manager works with SAT

If you enjoyed this link, you may also be interested in the https://github.com/pubgrub-rs/pubgrub project and its longform documentation at https://pubgrub-rs-guide.netlify.app/ we would love help.

It feels like reasonable, if you could download different versions, SAT should be able to always give an answer, then it does not make much of sense to use SAT.

In order to always be able to find a solution you either need to not have "these two versions are not compatible" rules (like npm) or not have "these two version constraints do not overlap" (like go). Otherwise you're resolver should be NP-complete and a SAT library might be useful.

SAT is a remarkably general framework. It consists of variables and clauses. If there is a solution each variable must be set to either true or false. Similarly if there is a solution one literal in each clause needs to be true. This is sufficient to model any binary operation. Each bit is variable, and there's a clause ensuring each connection. Considering modern programs are "just" operations on bits in theory SAT can solve anything. Alternatively, you can model circuits directly with the variable for each wire which either has power (true) or does not have power (false) then all connections get modeled with clauses. So any circuit can be modeled in SAT and computers are "just" circuits. So almost anything can be modeled as an SAT problem. Whether SAT solvers can find a solution to that problem is a different story.

So how do we model dependency resolution as an SAT problem.

1. We create a variables that represents each package version which is set to "true" if the packages in the lock file and "false" if it is unused.

   cargo/crates/resolver-tests/src/lib.rs

   Line 256 in 633929d

   let var_for_is_packages_used: HashMap<PackageId, varisat::Var> = registry

2. At this point is possible to select every version of every package. So we need to mark certain versions as incompatible with each other. We could add a clause not A, not B for all A and B that are incompatible, but there are more efficient ways to do it for large numbers of versions.

   cargo/crates/resolver-tests/src/lib.rs

   Line 198 in 633929d

   fn sat_at_most_one(solver: &mut impl varisat::ExtendFormula, vars: &[varisat::Var]) {

   if you want "at most one version per package" then you have these constraints for all versions of the package. But for cargo we want "at most one version per compatibility range per package" so we do

   cargo/crates/resolver-tests/src/lib.rs

   Line 271 in 633929d

   sat_at_most_one_by_key(

3. Now different versions can conflict, but dependencies might not be selected. So we need to add clauses that ensure that if a package is selected for each dependency a version that satisfies that dependency is selected.

   cargo/crates/resolver-tests/src/lib.rs

   Line 289 in 633929d

   // active packages need each of there `deps` to be satisfied

I hope that helps you understand what is going on. Feel free to turn this into comments in the code to help answer questions going forward! And if you have follow-up questions please ask!

[ShuiRuTian]

Cooooool, especially about https://pubgrub-rs-guide.netlify.app/. Looks really interesting.

Need some time to read the doc/code to figure out how it works. Would like to contribute a README if I am ready in future!

[Eh2406]

@epage , what is correct tag for "help wanted" these days?

[epage]

S-accepted

[weihanglo]

Assumed Eh2406 was going to tag this as S-accepted for documenting things discussed above, so I went ahead and did that.