Dependency Resolution as Backtracking Search Over Version Sets

A manifest does not name the packages that will be installed. It names ranges: >=1.4,<2, ^0.9.3, ~=3.1. Turning those ranges into a concrete set of artifacts is a search problem, and the search is the part of a package manager that decides whether an install succeeds at all. The output is one assignment of a single version to every package reachable from the root manifest, such that every declared constraint is satisfied by that assignment.

The naive procedure is to walk the dependency list and take the newest version that satisfies the constraint currently being considered. That procedure is correct only when constraints never interact. They interact constantly, because two packages can depend on the same third package with ranges that do not overlap, and because the version chosen for a package determines which constraints its own dependencies contribute.

The diamond that defeats greedy selection

Consider a root that depends on alpha and beta. Version 4.0 of alpha requires gamma >=2,<3. Version 2.0 of beta requires gamma >=3,<4. Taking newest-first, the resolver fixes alpha 4.0, then beta 2.0, then looks for a gamma that satisfies both ranges. The intersection of [2,3) and [3,4) is empty. No version of gamma works.

The resolver must now reconsider a decision it already made. Dropping to beta 1.x might relax the constraint on gamma, but only if beta 1.x declares a different range or none at all. If every beta version in the compatible line requires gamma >=3, the resolver must go back further and try alpha 3.x, which may accept gamma 2.x. A greedy resolver that never revisits earlier choices reports a conflict that a correct resolver would avoid, or worse, installs a set that violates a constraint it never rechecked.

The number of candidate sets grows multiplicatively. Ten packages with twenty versions each give $20^{10}$ combinations before any pruning, roughly $10^{13}$. Enumeration is not a strategy; the resolver needs to prove large regions of that space irrelevant without visiting them.

Partial assignments and unit propagation

A resolver state is a stack of decisions plus a set of derived facts. Each decision fixes one package to one version. Fixing a version adds that version’s dependency constraints to the pool, and the pool is then closed under propagation: if a constraint on a package admits exactly one remaining candidate, that candidate is forced, and its own dependencies are added in turn. Forcing cascades until no constraint is unit.

The representation that makes propagation cheap treats each constraint as a set of allowed versions and each conflict as an incompatibility: a conjunction of terms that cannot all hold. A term is a positive statement about one package, such as “gamma is in [3,4)” or “alpha is not 4.0”. Unit propagation over incompatibilities derives new incompatibilities: if all but one term of an incompatibility are known true, the remaining term must be false. When an incompatibility has all terms true, it is a conflict, and the derivation that produced it is a proof that the current decision stack is inconsistent.

This framing matters because it makes the reason for a failure explicit and reusable. A resolver that only knows “this branch failed” must try every sibling branch under the same parent. A resolver that knows which decisions caused the failure can skip entire subtrees.

Backjumping instead of chronological backtracking

Chronological backtracking pops the most recent decision and tries the next candidate for that package. If the conflict was caused by a decision eight levels down the stack, that is wasted work: the last several decisions had no bearing on the failure, and every combination of their alternatives will fail identically.

Conflict-driven backjumping computes the decision level at which the conflict’s causes were introduced and returns directly to that level, discarding the intermediate decisions. It also records the derived incompatibility, so a later branch that recreates the same partial assignment fails immediately rather than re-deriving the conflict. The two mechanisms together are the same idea as clause learning in a SAT solver, applied to version ranges instead of boolean literals.

The learned incompatibility must be expressed in terms general enough to be useful and specific enough to be sound. A conflict involving alpha 4.0 and beta 2.0 over gamma yields an incompatibility stating that alpha 4.0 and beta 2.0 cannot coexist, which then prunes every branch containing both. Because versions form ordered ranges rather than arbitrary sets, resolvers can widen the learned fact to a range: if alpha >=4 conflicts with beta >=2, the learned incompatibility covers an interval instead of a point.

What the search does not optimise

Resolution answers satisfiability, not optimality. Once a complete assignment is found, the search stops; nothing guarantees that the chosen set is the newest overall, the smallest, or the closest to the previous lockfile. Preference order affects which model is found first, and that is a heuristic. Two resolvers given identical manifests can legitimately return different sets, both correct.

A useful consequence is that resolution is order-dependent in a way manifests do not express. A resolver that prefers newest versions everywhere tends to satisfy constraints by lowering versions only where forced, which produces deep downgrades late in the search. Some resolvers instead prefer the fewest distinct versions of each package, which reduces duplication but can pull an older version of a widely used library into the graph.

The general problem is NP-hard: version selection can encode boolean satisfiability by treating “install package P at version v” as a literal and dependency constraints as clauses. Practical resolvers avoid the worst case through propagation, learned incompatibilities, and the empirical structure of real dependency graphs, where most constraints are loose and conflicts cluster around a small number of packages.

Where resolution breaks down

Four failure modes recur.

Cycles are legal in the graph but must not be re-expanded. A package already fixed by a decision is not a new node; treating a -> b -> a as fresh work yields non-termination on graphs that have a perfectly consistent solution.

Constraints with exclusions break interval reasoning. A range like >=1.0,!=1.4.2,<2.0 is a union of intervals, and code that assumes a single contiguous interval will either accept 1.4.2 or reject everything above it. Pre-release handling is a second source of the same bug: whether 2.0.0-rc1 satisfies >=1.0 depends on ecosystem policy, and treating pre-releases as ordinary versions makes resolvers pick them by accident.

Yanked or withdrawn versions create a gap between what the index advertises and what may be selected. A yanked version remains resolvable if a lockfile already names it, but must not be chosen fresh; a resolver that ignores the distinction silently resurrects artifacts the publisher intended to retire.

Finally, the search cost is dominated by the number of candidate versions per package, not by the number of packages. A package with several thousand published versions turns each constraint into a wide branch. Real resolvers mitigate this by fetching only metadata for candidate versions, ordering candidates by version precedence, and pruning versions whose declared dependencies already contradict the current partial assignment. The metadata question is taken up in Registry Index Metadata and Resolution Without Downloading Artifacts, and the constraints being propagated are defined in Version Precedence and the Semantics of Range Operators.

A compact implementation shows the shape of the search. It ignores conflict learning, which is what separates a textbook backtracker from a usable one.

def resolve(pool, constraints, chosen):
    # constraints: {name: [(lo, hi), ...]} half-open intervals
    if not constraints:
        return dict(chosen)
    name = min(constraints, key=lambda n: len(candidates(pool, n, constraints[n])))
    for version in candidates(pool, name, constraints[name]):
        merged = dict(constraints)
        del merged[name]
        chosen[name] = version
        ok = True
        for dep, rng in pool[name][version]:
            merged[dep] = merged.get(dep, []) + [rng]   # copy: siblings must not see it
            if dep in chosen and not satisfies(chosen[dep], rng):
                ok = False
                break
        if ok:
            result = resolve(pool, merged, chosen)
            if result is not None:
                return result
        chosen.pop(name, None)
    return None

The min over remaining packages is the branching heuristic; choosing the most constrained package first prunes hardest. candidates filters the version list against every accumulated range, and the early satisfies check catches contradictions before descending. The recursion explores the same tree a full solver does, minus the memory of why branches failed.

The practical lesson is that resolution is a solver, and solvers fail informatively. When a set of constraints has no model, the useful output is a minimal subset of the manifest that cannot be satisfied together, which is a separate derivation problem from finding a model. A resolver that reports only “no solution” leaves the manifest author to bisect by hand.