Finding a minimal set of package versions in a dependency graph with constraints

Question

Suppose you have a dependency graph of "packages" registered in the ecosystem of a given programming language. We can model each package as a tuple (name, version) where name is the package name (like Plots) and version is a semantic version number (like 1.2.3).

Each package has a set of dependencies, which may include constraints. Perhaps Plot-1.2.3 depends on JSON with a constraint >= 1.0 && < 3.0. Thus, there could be a number of JSON-X.Y.Z versions that are compatible with Plot-1.2.3.

The goal of this problem is to construct a "minimal" set of nodes to form a useful package snapshot.

Let's define a "useful" package snapshot as following:

1. It contains the latest version of every package.
2. Every package in the snapshot is "resolvable" (EDIT: as long as it's resolvable in the original ecosystem), i.e. the snapshot must include a compatible version of every necessary dependency of that package.
3. Every two packages in the snapshot are "pairwise resolvable," meaning that if there is a working set of dependencies to install them simultaneously in the original ecosystem, then there is also such a working set in the snapshot. (EDIT: note that when you're installing a set of packages, you only get to choose one version of a particular dependency package. Thus, if packages P and Q both depend on dependency D, pairwise resolvability means that there must be one single version of D compatible with both P and Q in the snapshot, as long as such is true in the full ecosystem.)

By this definition the full ecosystem is a useful snapshot. But the key part of this goal is "minimal." I want to find the smallest useful package snapshot that satisfies the rules above. I feel like there must be some prior art or theory that can help here. Graph coloring? Satisfiability? Please help :)

---

In case it's of interest, this is a real problem -- I want to package such a snapshot in the Nix package manager, so that a user can express something like "Please give me an environment with packages A, B, and C" and get a working environment with the latest version of those packages, as long as such is possible. There are about 80,000 nodes in the real graph. The solution doesn't need to be perfectly optimal but the smaller I can get it, the better.

Answer 1

One standard approach for package managers these days seems to be to use a SAT solver (or ILP solver). That seems like a plausible solution. All of your requirements can be expressed in SAT (or ILP).

If you use SAT, you will need to constrain the number of packages selected, using a cardinality constraint: see Reduce the following problem to SAT (also Encoding 1-out-of-n constraint for SAT solvers has a few methods that can be generalized to this). Then, do binary search to find the minimal number of packages that can be selected. If you use ILP, see Express boolean logic operations in zero-one integer linear programming (ILP) for tips on expressing your constraints within ILP.

One approach to enforce 2-resolvability is to add a constraint for every pair of packages that they be simultaneously resolvable. However, a more efficient way might be to use lazy enforcement: initially, ignore those constraints, and solve the SAT/ILP instance without such a restriction. Then, check the resulting solution for any violations of 2-resolvability. For each pair of packages $P,Q$ that fail to be 2-resolvable with that solution, add a new constraint that $P,Q$ must be simultaneously resolvable, then solve the resulting modified SAT/ILP instance. Repeat until all such pairs are resolvable.

Another approach is to ask that there is a high probability that the set $\mathcal{S}$ of packages is simultaneously resolvable, where $\mathcal{S}$ is chosen according to some probability distribution that approximately mimics the packages a user is likely to ask to install. To achieve that, one approach would be to randomly sample $n$ such sets, $S_1,\dots,S_n$, from this distribution, then add constraints requiring that all of $S_1,\dots,S_n$ be simultaneously resolvable. Another variant of that is to add a constraint that requires that at least $0.9n$ of $S_1,\dots,S_n$ be simultaneously resolvable (using another cardinality constraint, if you are using SAT).