Pruning the Search Space
Learning through Conflicts - the CDCL aspect of Buckaroo's Resolver
Conflicts in the resolution process are a learning opportunity. By leveraging information from failed paths, we can prune the search space.
There are many reasons why the resolution process may lead to a conflict.
In this example the resolver tries to find a suitable package version for
B@all(2.x 3.0). This might succeed or fail for one of the following reasons:
- Package identifier
Bdoes not exists -
2.xyields no versions -
3.0yields no versions - There are no common versions between
2.xand3.0 - A conflict occurs in a transitive dependency of
B(recursion)
We will only look at case (4) here, since this covers the most significant aspects of the algorithm.
A failure of all(2.x 3.0) means that the intersection of packages described by [email protected] and [email protected] is empty ([email protected] ∩ [email protected] ⇔ Ø).
We can use this clause for pruning but also deduce more clauses that fail:
- We know that
[email protected]implies[email protected] - Hence we know that the combination of clauses also fails:
[email protected] + [email protected].
The set of clauses are called unsatisfiable cores and we can skip over every manifest that is contained by any of those cores.
We benchmarked both approaches and found that it depends on the dependency graph. In pathological cases, switching from one approach to the other can change increase the resolution time from seconds to hours.
Buckaroo needs to work reasonably well for all cases, so it takes a different approach. Instead of always searching breadth or depth first, it tries to discover unresolvable cores as quickly as possible. This is done by prioritizing constraints that are more likely to fail, determined by the number of terms and some simple heuristics. For example, a version constraint is (usually) more specific than a branch constraint.
This approach optimizes for the discovery of unsatisfiable cores, which enable earlier pruning of the search space.
From the resolver's perspective, all package versions that have the same manifest are interchangable. Thus to avoid repeated work, package versions are grouped by their manifest hash in order to share dependency graphs.