Backtracking Resolution

Modern resolvers (cargo, pip 2020+, poetry, dart) use backtracking SAT solving:

def solve(packages, constraints):
    if no constraints to satisfy: return current solution
    pick a package P with unsatisfied constraints
    for each version V of P (highest first, matching all current constraints):
        try installing V
        recurse: solve with updated constraints
        if recursion succeeds: return solution
    return FAILURE  # backtrack

The "pick highest first" heuristic finds a solution fast when one exists. The backtracking handles transitive conflicts: maybe the highest version of package A requires an incompatible version of B; backtrack and try A's second-highest, which might pull in a compatible B.

A naive implementation can be exponentially slow on adversarial inputs. Real solvers use:

• Conflict-driven clause learning (CDCL): when a conflict is found, add a "no-good" clause that prevents revisiting the same dead end.
• Heuristics for variable order: solve "high-impact" packages first.
• Partial order: keep packages with FEWER candidates resolved first ("most constrained first").

PubGrub (used by cargo and pubspec since 2018) is the modern algorithm. The paper is "PubGrub: Next-Generation Version Solving" by Natalie Weizenbaum.

For this lesson: a simple recursive-with-backtracking resolver.