Conflict-Driven Backtracking in Dependency Resolution

The straightforward resolver is a depth-first search. Pick an unsatisfied package, order its candidate versions from newest to oldest, try the first, propagate the consequences, and recurse. On failure, undo the most recent choice and try the next candidate. It is easy to write and it is correct, in the sense that it will find a solution if one exists. It is also, on inputs that appear in practice, capable of taking longer than anyone is willing to wait, because most of the work it does is re-deriving failures it has already seen.

Undoing the wrong decision

Consider a root that depends on A and Z. A has forty published versions, each of which depends on a different version of Z. Z has two versions, and only 1.x is compatible with the root’s own requirement. Suppose the resolver picks A first, newest version, which requires Z 2.x. It then picks Z, discovers the conflict with the root’s requirement, and backtracks. Chronological backtracking undoes the Z choice, finds no other Z candidate, then undoes the A choice and tries the next A version, which also requires Z 2.x. Forty A versions later, the search concludes that no solution exists, having learned nothing from the first thirty-nine failures.

The information was available at the first failure: this version of A is incompatible with the root’s requirement on Z, and that incompatibility does not depend on anything else. A resolver that records the reason for a failure, rather than only the fact of it, avoids re-deriving it. Recording reasons is the entire content of conflict-driven resolution, and the data structure that holds them is an incompatibility.

An incompatibility is a forbidden combination

A term is a statement about one package: either “this package is at a version satisfying this range” or its negation. An incompatibility is a set of terms that cannot all hold at once. The declaration that package P at version 1.4.2 depends on Q in the range ^3 gives rise to the incompatibility {P 1.4.2, not Q ^3}: it is impossible for P to be 1.4.2 while Q is outside ^3. Negation is what makes the encoding uniform, because every fact about the world becomes a forbidden set rather than a positive assertion.

The partial solution is a stack of assignments, each tagged with a decision level. A decision is a choice the resolver made; a derivation is a consequence forced by unit propagation. Each derivation records the incompatibility that caused it, which is what makes conflict analysis possible later. The partial solution is always consistent with every incompatibility recorded so far — that is the invariant the algorithm maintains, and a violation of it is exactly a conflict.

Unit propagation is the workhorse. For each incompatibility, count how many of its terms are satisfied by the partial solution. If all of them are satisfied, the incompatibility is violated and there is a conflict. If all but one are satisfied and the remaining one is undecided, the remaining term must be false, so its negation is derived and added to the partial solution. In the example above, once P 1.4.2 is decided, the incompatibility {P 1.4.2, not Q ^3} has one satisfied term and one undecided term, so the resolver derives Q ^3 without any search.

This is where the compression relative to a boolean encoding shows up. A term can cover an arbitrary range of versions, so “Q ^3” is one term rather than one literal per version — the expansion of that syntax into a set is described in Version Ranges as Sets of Versions. The at-most-one-version constraint that a SAT encoding must state explicitly is implicit: two terms over the same package with disjoint ranges cannot both hold, and the incompatibility machinery handles that by construction rather than by clauses.

Conflict analysis and backjumping

When propagation produces a conflict, the resolver does not simply pop the stack. It takes the violated incompatibility and the derivations that satisfied its terms, and resolves them: for the term satisfied at the highest decision level, find the incompatibility that derived it, and merge the two sets by removing the term and adding the other incompatibility’s terms. The result is a new incompatibility that explains the conflict in terms of decisions rather than in terms of intermediate derivations.

Resolution repeats until the derived incompatibility contains exactly one term at the current decision level. That term identifies the decision responsible for the conflict. The resolver then backjumps to the second-highest level present in the derived incompatibility — not to the immediately preceding decision — and derives the new facts there rather than at the level where the conflict surfaced. Because the learned incompatibility is retained, the combination it forbids is never explored again, and the subtree that would have re-derived the same conflict is pruned in one step.

In the forty-version example, the first conflict yields an incompatibility of roughly the form {A’s version range that requires Z 2.x, root’s requirement}. If the resolver can express that range as a single term — say “A >= 3.0” — the entire block of A versions is excluded at once and the search ends after one conflict instead of forty. Whether such a compact term exists depends on how the versions’ requirements are distributed, which is why the encoding uses ranges and not individual versions.

The correspondence with conflict-driven clause learning in SAT is direct: decisions are decisions, derivations are implied literals, the learned incompatibility is a learned clause, and the backjump level is computed the same way from the second-highest level in the clause. Package resolution differs in the structure of its literals, not in the shape of the algorithm.

The learned set is also the explanation

Because incompatibilities accumulate, the final state of the resolver after a failed search is a proof that no solution exists. Rendering that proof is the difference between an error message that says “could not resolve dependencies” and one that says which requirement forced which choice and where the cycle of constraints closed.

A useful rendering walks the derivation graph from the root requirement to the conflict. Each step is an incompatibility with a human-readable cause: a dependency declaration, a version’s own requirement, or a derived conclusion. PubGrub’s documentation describes this as reporting the derivation chain, and the practical effect is that the user sees the shortest path through the constraint graph that leads to failure rather than a dump of every package examined.

This has a cost in memory. The number of retained incompatibilities grows with the number of conflicts, and each one holds terms with ranges. Implementations bound the work by limiting the number of conflicts or the number of versions tried, and report a timeout rather than continuing. A resolver that never bounds its search can be made to run for an extremely long time by an adversarial registry, which is a denial-of-service surface as much as a usability problem.

Where the search still explodes

Learning eliminates re-derivation of identical conflicts, but it does not make the problem tractable in the worst case. The decision version of dependency resolution is NP-complete, as Dependency Resolution as a Satisfiability Problem sets out, so no amount of engineering removes the exponential bound. What learning does is move typical instances from “exponential in the number of packages” to “roughly proportional to the number of conflicts actually encountered”, and typical instances have few conflicts because most packages have wide compatibility.

The remaining hard cases have a recognisable shape. Graphs where every package constrains a single shared dependency at incompatible ranges generate many conflicts that differ only in which package was decided first. Graphs with large version counts and narrow ranges generate long propagation chains before any conflict appears. And graphs where a solution exists but requires choosing an old version of a central package produce a search that must exhaust the newer candidates first, since the ordering policy prefers newest.

Ordering the decisions matters for all three. Choosing the package with the fewest remaining candidates first, and propagating fully before making the next decision, reduces the branching factor at each level. Neither heuristic changes the worst case, and both are cheap to compute, which is why they appear in every implementation.

def propagate(incompat, solution):
    """solution: {package: (lo, hi)} decided or derived ranges."""
    undecided = []
    for pkg, (lo, hi) in incompat:
        cur = solution.get(pkg)
        if cur is None:
            undecided.append((pkg, lo, hi))
        elif cur[0] >= lo and cur[1] <= hi:
            continue          # term satisfied
        else:
            return None       # term already false: incompatibility inactive
    if len(undecided) == 1:
        pkg, lo, hi = undecided[0]
        return (pkg, lo, hi)  # caller derives the negation
    return None

The snippet omits the resolution step that turns a conflict into a learned incompatibility, and that omission is where most of the engineering lives. Propagation alone gives a solver that is correct and only occasionally fast; the learning step is what makes the difference between a resolver that finishes and one that is killed by its own timeout.

Choosing between this and a simpler policy

Conflict-driven resolution is worth its complexity when the ecosystem permits wide version ranges and deep graphs, because those are the conditions that produce conflicts. It is hard to justify when the policy is minimal version selection, which by construction never backtracks: taking the maximum of declared minimums is a single pass, and no failure can arise from a choice, only from a missing module. The trade is expressiveness against predictability. A backtracking resolver can satisfy constraints that a monotone policy cannot, at the cost of a search whose duration is not bounded by the size of the graph.