Resolution as Constraint Search: Why Dependency Solving Is NP-Hard

A resolver is handed a set of packages, a set of candidate versions for each, and a set of version requirements that appear only if a particular candidate is selected. It must return an assignment of exactly one version per selected package such that every requirement is satisfied, or prove that no such assignment exists. The second half of that sentence is what makes the problem hard: an installer that reports “conflict” when a solution exists is as wrong as one that installs a broken graph.

The difficulty is structural rather than accidental. Dependency solving is the canonical example of a problem whose constraints are conditional on the choices being made, and conditional constraints put it in a complexity class where no general polynomial algorithm is known.

Constraints that appear only after a choice

Consider a graph with three packages. Package app requires liba at any 1.x or libb at any 1.x. liba 1.x requires core exactly 1.0. libb 1.x requires core exactly 2.0. core publishes 1.0 and 2.0, and nothing else.

If app’s requirement were a plain conjunction, the problem would decompose into independent subproblems: pick a liba, pick a core for it, repeat. But the requirement is a disjunction, and which branch is taken determines which core constraint exists. Selecting liba produces the clause “core = 1.0”; selecting libb produces “core = 2.0”. The two branches are mutually exclusive, and the constraint on core is a function of the branch.

This shape is what a resolver actually faces, and it is why naive approaches fail. A greedy resolver that walks requirements in order and picks the newest satisfying version will succeed on this graph if it happens to try liba first and fail if it tries libb first, with no way to tell which was right until it backtracks. A resolver that only propagates constraints forward, without the ability to revisit an earlier choice, cannot recover.

The formal statement: given a set of packages with finite version sets, a set of dependency clauses, and a distinguished root package, decide whether an assignment exists that selects the root and satisfies every clause generated by the selection. This is the problem known in the literature as the package management problem, and it is NP-complete. The reduction runs from boolean satisfiability: encode each variable as a package with two versions, each clause as a package requiring one of the literals, and satisfiability becomes selection.

Why the reduction matters in practice

NP-completeness is often treated as a curiosity, a fact to mention and move past. Here it has operational content. It says that no resolver can be both complete and fast in the worst case, so every real resolver trades one for the other, and knowing which trade a given tool makes predicts its failure behaviour.

The three common positions:

Complete and exponential. Enumerate and backtrack, with memoisation of failed partial assignments. Complete: it will find a solution if one exists. Exponential in the worst case, but real graphs are not adversarial. Most resolvers that ship with a package manager sit here, with pruning heuristics that make the blowup rare rather than absent.

Incomplete and fast. Greedy selection with local repair: take the newest version, propagate, and when a conflict appears, relax the newest constraint or downgrade the offending package. Fast and predictable, but it can miss solutions, particularly when the solution requires choosing an older version of a package that is not the one that reported the conflict. This is the failure mode reported as “the resolver says X conflicts with Y” when both have a compatible pair.

Incomplete and explicit. Declare a documented restriction on the input — no cycles, one version per major, no disjunction beyond a depth — and reject anything outside it. Predictable, and honest about its limits, but it rejects legitimate graphs.

A resolver’s error message quality is largely determined by which of these it is. An incomplete resolver cannot distinguish “no solution” from “no solution found by this strategy”, and the honest wording for its failure is “could not find a solution”, not “there is no solution”.

Encoding as SAT and the cost of the encoding

The complete approaches generally translate the problem into propositional satisfiability and hand it to a CDCL solver. The encoding is direct: one boolean variable per (package, version) pair, clauses asserting that at most one version of each package is selected, clauses asserting that selecting a version implies selecting a version of each of its dependencies, and clauses for the root.

# Sketch of the encoding, not a solver.
# catalog: {name: {version: [(required_name, [allowed_versions]), ...]}}
# A clause is a list of literals; a literal is (name, version, positive).
def encode(catalog):
    clauses = []
    for name, releases in catalog.items():
        versions = list(releases)
        # At most one version of a package may be selected.
        for i, vi in enumerate(versions):
            for vj in versions[i + 1:]:
                clauses.append([(name, vi, False), (name, vj, False)])
        # Selecting the package at all implies selecting some version.
        clauses.append([(name, v, True) for v in versions])
        for version, requirements in releases.items():
            # Choosing a version implies every requirement it declares.
            for req_name, allowed in requirements:
                clauses.append([(name, version, False)] +
                               [(req_name, v, True) for v in allowed])
    return clauses

The size of that encoding is the first cost. Pairwise exclusion for a package with $k$ versions emits $k(k-1)/2$ clauses, so a package with a thousand published versions contributes roughly half a million clauses before any dependency is considered. Solver-friendly encodings use sequential or commander variables to reduce this to linear size, at the cost of introducing auxiliary variables.

The second cost is that the encoding discards information the solver cannot recover. SAT returns an assignment or a proof of unsatisfiability in terms of boolean variables, and mapping that proof back to a human-readable statement about package versions is a separate, non-trivial step. A user who receives “unsatisfiable” without a minimal explanation is not helped, and computing a minimal unsatisfiable core is itself expensive.

The third cost is time. The worst-case bound is exponential, and even in the average case a solver invoked during installation adds latency to a command that users expect to be interactive.

Conflict-driven learning applied to versions

The middle path, used by several modern resolvers, borrows the CDCL idea without the full SAT encoding. The resolver maintains a partial assignment plus a set of incompatibilities, where an incompatibility is a conjunction of terms that cannot all hold — “version 2.0 of core together with version 1.x of liba”. Requirements are translated into incompatibilities, and the search proceeds by unit propagation over that structure.

When propagation derives a conflict, the resolver walks back through the derivation to find the root cause, records a new incompatibility that summarises it, and backjumps to the decision level where the cause was introduced. The learned incompatibility prevents the same conflict from being re-derived elsewhere in the search, which is what turns a naive backtracker into something that handles realistic graphs quickly.

The advantage over SAT encoding is that the terms stay at the level of package versions throughout, so explanations are natural: a reported conflict is a list of version choices that cannot coexist, and it is exactly the incompatibility the resolver derived. The advantage over greedy selection is completeness within the search space it explores.

The limitation is that the incompatibility language is restricted relative to full propositional logic, which makes the algorithm easier to reason about but means some constraint shapes must be encoded awkwardly. And the worst case remains exponential: a graph can be constructed whose resolution requires exploring exponentially many branches, and no amount of learning removes that bound. What learning does is make the exponential cases rare enough that no one constructs them by accident.

What makes real graphs tractable

The saving grace is that published dependency graphs are not adversarial. Several properties hold consistently and each one cuts the search space:

Version sets per package are small relative to the total number of packages, and most requirements are intervals rather than disjunctions, so propagation rarely branches. Disjunctions, when present, are usually two-branch alternatives between a native implementation and a pure one, and both branches typically admit the same version of shared dependencies.

Most packages have a single dominant version in a given graph, because dependents converge on recent releases. The resolver’s job is then mostly confirming that the obvious assignment works.

The number of distinct packages in a graph is bounded by practical limits — a few hundred for a large application, a few thousand for a monorepo — and the constraint graph is sparse: each package depends on a handful of others.

Where these properties fail, resolution becomes slow or unsatisfiable, and the failure is usually traceable to a specific structural feature. A dependency cycle between packages that each require the other at a range that only one version satisfies forces the resolver to consider the cycle as a unit. A package that publishes a new version for every commit creates version sets large enough to dominate propagation. Deeply nested optional dependencies multiply branches.

The unsatisfiable case is the common complaint

Users encounter the resolver most often when it refuses. The complaint is not that resolution is slow but that the refusal is unexplainable, and the explanation requires the resolver to report the derived incompatibility rather than a summary.

A minimal report names the packages whose constraints cannot be reconciled and the version sets involved: “app requires liba >=2.0, libb requires liba <2.0, no version of liba satisfies both”. That is the intersection test from the range algebra, performed over the whole graph rather than pairwise. Producing it requires tracking which requirement introduced each term, which is why resolvers that report only “conflict” are usually the ones that discard provenance during propagation.

The complementary failure is a resolution that succeeds and should not. If a resolver picks versions that satisfy the declared ranges but violate an unstated invariant — two packages that both register a global, or that both own the same file — the graph is technically valid and practically broken. No constraint system over versions can detect that, because the constraint is not in the versions. This is why install-time lifecycle execution is a separate risk surface from resolution itself.