Inefficient backjumping/backtracking case

[frostming]

I just want to record an inefficient case for backjumping(or backtracking) process.

Given this criterion of package A, the top is pinned most recently:

A<7 (from B)
A<7 (from C)
A<7 (from D)
A>=6 (from E)

In the current round we are trying to pin F and F depends on A<6, obviously it introduces a conflict. But the resolver has to exhaust all versions of F to realize F is not able to resolve at this point, and starts to back jump(in this case backjump is similar to backtrack because all packages are relevent here).

The next step is to revert B and try to find another working version, but it fails, then it goes on with C, D... Imagine A is a common dependency of many packages and each has a lot of versions. The resolver has to exhaust all versions of B,C,D and find out they are not helpful at all, because the critical package is E. The process will look like following:

1. F@{1...N}  # REJECT
2. B@2 -> F@{1...N}  #REJECT
3. B@3 -> F@{1...N}  #REJECT
...
4. C@2 -> B@{1...M} -> F@{1...N}  #REJECT
5. C@3 -> B@{1...M} -> F@{1...N}  #REJECT
...

That is a NxMxOxP... complexity. Is it possible to immediately find E that needs to pop out from the state without adding more methods to resolver?
@notatallshaw

[notatallshaw]

It depends, if B, C, and D are not pinned because they form a series of linear dependencies (B -> C -> D), then a learning algorithm, like PubGrub, should be able to significantly speed up discarding entire branches when backtracking. Learning algorithms do this by adding incompatibilities as they iterate through the resolution process, which they never remove.

pubgrub.rs is quite limited in what it means by versions and version ranges, compared to Python packaging versions and specifiers, though somehow mixology has implemented PubGrub.

But resolvelib is very generic in what it allows. A Criterion represents the state of the resolution for a given Requirement, and can really mean almost anything as long as the provider can determine whether it can produce a Candidate that satisfies the current set of criteria. So it's not clear to me if it's possible to extend resolvelib to support learned incompatibilities without breaking its generality, and if it is possible whether a new method would need to be added to the provider interface.

That said, in the worst case, if B, C, and D are pinned because they form a series of linear dependencies (B -> C -> D), a learning algorithm doesn't help, you still need to check each version of B, C, and D. I do have this idea that the provider could restart the resolution when it detects such a pathological situation and know to prefer F and E over B, C, or D, but this would definitely require a new method on the provider.

P.S. This is all based on my understanding and intuition, I am not a SAT solver expert, beyond working on Python packaging resolution problems.

[frostming]

a series of linear dependencies (B -> C -> D)

There are no such dependency relationship, B, C, D are independent packages that all depend on A, and get pinned in reversed order.

Yeah maybe we require another provider method to modify the state, instead of simply popping the last resolved item, while the latter can serve as a default implementation.