Dependency Resolution as a Satisfiability Problem

The question “is there a set of versions satisfying all constraints” is a decision problem with a yes-or-no answer, and it can be handed to a general-purpose solver unchanged. Doing so is instructive for two reasons: it gives a precise account of why resolution is hard, and it shows which parts of the problem the hardness actually covers. The encoding also makes explicit a constraint that resolvers usually enforce silently, namely that a package gets one version.

One variable per package version

Fix a finite universe of candidates: every version of every package that the walk could reach. Introduce a boolean variable for each pair. Assigning true to variable A@1.4.2 means the installation includes that version of A.

The formula has three families of clauses. The first says that each root requirement must be satisfied: for a root dependency on A with range r, a clause containing every variable A@v where v satisfies r. If the range admits no published version, the clause is empty, which is unsatisfiable by definition and produces an immediate and correct verdict.

The second family encodes dependencies. For a version A@a whose manifest requires B in range r, the clause ¬A@a ∨ B@b1 ∨ B@b2 ∨ … lists every candidate version of B in r. If the list is empty, the clause is the unit ¬A@a, which forbids that version of A outright. Transitivity needs no separate machinery: every version in the universe contributes its own implication, and the closure emerges from the conjunction.

The third family enforces one version per package: for every pair of distinct versions of A, the clause ¬A@ai ∨ ¬A@aj. Writing these pairwise costs n(n−1)/2 clauses for a package with n versions, which for a package with a hundred published versions is several thousand clauses. A sequential encoding introduces auxiliary variables and brings the count down to roughly 3n, at the cost of a larger variable set. Both are standard, and the choice matters only for solver performance.

def encode(candidates, root_reqs, deps):
    """candidates: {name: [versions]}
       root_reqs:  {name: range_pred}
       deps:       {(name, ver): {dep_name: range_pred}}"""
    var, clauses = {}, []

    def v(name, ver):
        key = (name, ver)
        if key not in var:
            var[key] = len(var) + 1
        return var[key]

    for name, pred in root_reqs.items():
        clauses.append([v(name, ver) for ver in candidates[name] if pred(ver)])

    for (name, ver), reqs in deps.items():
        for dep, pred in reqs.items():
            head = [v(dep, d) for d in candidates.get(dep, []) if pred(d)]
            clauses.append([-v(name, ver)] + head)   # empty head forbids the version

    for name, versions in candidates.items():
        for i, a in enumerate(versions):
            for b in versions[i + 1:]:
                clauses.append([-v(name, a), -v(name, b)])   # at most one version
    return var, clauses

The first family states the root requirements, the second carries each version’s own requirements forward, and the third is the at-most-one family whose clause count grows quadratically with the number of published versions.

Why the decision problem is NP-complete

Membership in NP is immediate: a proposed assignment of one version per package can be checked in time linear in the number of clauses, by evaluating each clause. A certificate is small relative to the input, and the check is mechanical.

Hardness comes from a reduction in the other direction. Take a 3-CNF formula with variables x1 through xn and clauses C1 through Cm. Build a package for each variable with exactly two versions, one meaning true and one meaning false. Build a package for each clause with three versions, one per literal, where the version corresponding to literal l requires the variable package at the version that makes l true. Add a root requirement on every clause package. A satisfying assignment of the formula corresponds to a selection: choose the variable versions according to the assignment, and for each clause choose a version whose literal is true, which exists precisely because the clause is satisfied. Conversely, any valid selection induces an assignment that satisfies every clause, since each clause package’s chosen version forces its literal’s variable to the satisfying value.

The at-most-one constraint is what makes the correspondence work, because it is the mechanism that forces a variable package to have one truth value. Without it, the solver could select both versions of a variable and satisfy every clause trivially, which is why an encoding that omits the constraint produces “solutions” that no installer can execute. This is the most common bug in hand-rolled encodings, and it is invisible until an instance that needs the constraint appears.

The reduction uses three versions per clause and two per variable, so the instance size is linear in the formula. That establishes NP-hardness, and with the membership argument, NP-completeness. The practical reading is that no algorithm known today decides all instances in polynomial time, and an implementation that appears fast on ordinary registries is exploiting structure rather than beating the bound.

Ranges versus literals

A resolver that works directly on ranges, as PubGrub does, avoids materialising one variable per version. Its terms denote sets of versions, and its incompatibilities are clauses over those terms. The formula it manipulates is exponentially smaller in the number of versions per package, and the propagation step reasons about interval intersection rather than clause satisfaction.

This is not a different complexity class; it is a different encoding of the same problem, and the encoding changes which instances are easy. A clause over “any version of A at or above 3.0” prunes a whole block of candidates in one step, where the boolean encoding needs a clause per version or a cardinality constraint. Conversely, the boolean encoding can express arbitrary combinations of versions across packages, which range terms cannot, so it is more general than the package-manager problem requires.

The lift from clauses to range terms is what Conflict-Driven Backtracking describes: the same propagation, conflict analysis, and learning, with the literal replaced by a set. Solvers built this way are still complete, still exponential in the worst case, and usually much faster on package graphs than a general SAT solver fed the full formula, because they never build the full formula.

Optimisation is a different problem

Satisfiability asks whether some assignment works. Package managers are asked for a good assignment: usually the newest versions, or the fewest changes from the previous lockfile, or the smallest download. Adding an objective turns the problem into optimisation, and the standard reductions apply. MaxSAT asks for an assignment maximising the weight of satisfied soft clauses; a pseudo-boolean or integer program can express the same preferences directly. OPIUM formulated package installation this way, with an objective over version preferences and a solver over the resulting constraints.

The distinction has a practical consequence. A CDCL solver returns the first assignment it finds, and the order in which it branches determines which one that is. “Newest first” branching tends to produce a newest-heavy solution, but it does not guarantee the optimal one, because the search stops at the first satisfying leaf rather than proving that no better leaf exists. Guaranteeing the newest possible version of a specific package requires solving once per candidate version, or adding a constraint that excludes all better solutions and re-solving, which multiplies the cost.

This is why production resolvers usually implement a policy rather than an optimum. Selecting the newest admissible version at each decision, with backtracking only on conflict, is a greedy strategy that is fast and predictable; the result is optimal under the ordering only when the greedy choice never has to be undone. The gap between “a solution” and “the best solution” is where most of the remaining engineering effort in a resolver goes, and it is the reason lockfile diffs can be large after a small change: a different first choice can lead to a different leaf.

What the hardness result does not say

NP-completeness is a statement about the worst case over all instances, and package graphs are not worst-case instances. They have structure: most requirements are wide, most packages are leaves, and the dependency relation is shallow relative to the number of packages. A typical application graph has a few hundred nodes and a branching factor near one, and a resolver explores a path rather than a tree.

The hard instances have specific shapes. One is a set of packages all constraining one shared dependency at mutually exclusive ranges, which forces the search to try each combination — the diamond pattern that Diamond Dependencies and Duplicate Versions describes from the installer’s side. Another is a registry where many versions of a package exist with nearly identical requirements, so that the search cannot distinguish candidates until late. A third is an unsatisfiable instance, where the solver must exhaust the space to prove that no assignment exists; the proof may be much longer than any solution would have been.

None of these require a malicious registry. They arise from ordinary publishing patterns, which is why the bound is worth knowing even though it rarely bites. The engineering response is not to seek a polynomial algorithm but to make the search’s cost proportional to the conflicts it encounters, to bound the work with a timeout, and to report the derivation when the bound is reached, so that the failure is actionable rather than a hang.

The encoding as a diagnostic tool

Even when no SAT solver is in the loop, the encoding is useful for reasoning about a resolver’s completeness. Any constraint the installer enforces must appear as a clause, or the resolver can return assignments the installer rejects. Any clause omitted for performance is a class of instance on which the resolver is incomplete, and knowing which class it is tells a maintainer when to distrust the answer.

The same lens explains why resolver bugs cluster around the at-most-one family and around optional dependencies. The first is the constraint that makes the problem a choice rather than a set; the second is the constraint whose truth value depends on the environment rather than on the graph. Both are easy to leave out of a mental model, and both produce solutions that look valid and fail at install time.