Heuristic mediation strategies like nearest-wins and highest-version-wins always produce some answer, even when it's wrong. What does it mean for a dependency resolver to use a SAT/constraint-solving approach instead, and what problem does that solve that pure heuristics can't?

## Greedy heuristics always answer Nearest-wins and highest-version-wins are both greedy, local heuristics: for each conflicting artifact coordinate, they apply one fixed rule — shallowest depth, or largest version number — and commit to that pick immediately, without ever going back to check whether the choice actually satisfies every requirement anywhere else in the graph. Crucially, **both strategies are total functions**: given any dependency graph, they always terminate with an answer, even if that answer violates something. If library `X` strictly requires exactly version 2.0 of library `Z`, and highest-version-wins resolves Z to 3.0 because something else in the graph asked for that, the heuristic doesn't notice or care that it just broke X's strict constraint — it simply produces 3.0 as the answer and the failure surfaces later, if at all, as a runtime error rather than a build-time diagnosis. ## The constraint-solving alternative A **SAT-style** (Boolean satisfiability) or general constraint-solving approach treats the problem completely differently: as a genuine constraint satisfaction problem. Each dependency requirement — 'project needs A version at least 1.0', 'A needs Z in a given range', 'B needs Z in a different range' — becomes a constraint over which package-version pairs can coexist in a valid solution. The solver's job is to find an assignment of exactly one version to each package such that every constraint in the whole graph is simultaneously satisfied, or to correctly prove that no such assignment exists. It does this via search: 1. pick a tentative version for a package; 2. propagate the consequences; 3. and if a later constraint is violated, backtrack and try a different choice instead of the one that led to the dead end. This is conceptually the same shape of algorithm used in Boolean satisfiability solvers, hence the name — and modern package-manager resolvers borrow real SAT-solving techniques, most notably the **PubGrub** algorithm (developed for Dart's package manager and referenced by several other ecosystems' resolver logic), which specifically adds conflict-driven clause learning: when the search hits a contradiction, it doesn't just backtrack blindly, it records why that combination failed as a new learned constraint so it never re-explores the same dead end, and can construct a clear, minimal explanation of the conflict for the developer. ## Why this exists Heuristics like nearest-wins and highest-version-wins were designed for an earlier era of shallower dependency graphs and looser version ranges; as ecosystems grew graphs with thousands of transitive packages and richer version-range syntax, the odds of a real, unsolvable-without-a-substitution conflict existing somewhere in a large graph went up substantially, and a greedy heuristic simply cannot detect that case — it will produce an answer regardless, and that answer might quietly violate someone's strict requirement. A constraint solver closes that gap: it can definitively say there is no version assignment satisfying both a given pair of requirements, and, critically, tell you exactly which requirements conflict, rather than shipping a broken build silently. ## What solving costs The trade-off is cost, in two senses. 1. **First, computationally:** exhaustive constraint search is, in the worst case, exponential — real-world dependency graphs are usually well-behaved enough that clause-learning search terminates quickly, but pathological graphs can make resolution genuinely slow, which is part of why solver-based package managers invest heavily in caching resolved lockfiles rather than re-solving from scratch on every install. 2. **Second, in developer experience:** a heuristic resolver's output is always 'here's what I picked,' simple to understand even if wrong; a constraint solver's failure output has to be engineered carefully to be readable, because a raw dump of an unsatisfiable constraint set from a naive encoding is close to useless to a human — this is exactly the UX problem PubGrub was built to solve, producing an explanation naming the specific conflicting requirements instead of an opaque search trace. ## Where each one puts the pain Failure modes in production differ accordingly: | Resolver | Where the mismatch surfaces | |---|---| | **Heuristic** | the failure is silent and appears at runtime as a version mismatch nobody flagged | | **Solver-based** | the 'failure' is usually loud and appears at install/lockfile-generation time as an explicit unsatisfiable-constraints error | That is strictly better for catching the problem early, but can be genuinely frustrating to resolve when the constraint set is large, or when it forces a developer to manually relax a version range or add an explicit override to break the impasse, which is the same kind of manual pinning lever heuristic resolvers also expose, just invoked in response to an explicit error rather than a silently wrong pick.