14
Package Dependency Resolution as 3-SAT Roberto Di Cosmo et al., 2005 — installing a set of compatible packages is NP-complete. Every modern package manager is a SAT solver in disguise.
Roberto Di Cosmo, at the University of Paris Diderot, with collaborators on the EU-funded EDOS project, formally proved that the package installation problem in real-world Linux distributions is NP-complete. Given a repository of packages with version constraints, dependencies, and conflicts, decide whether a given set of user-selected packages can be installed simultaneously. Di Cosmo encoded the problem as 3-SAT for both the Debian (.deb) and Red Hat (.rpm) constraint languages, with reductions tight enough that real package managers were observed to time out on adversarial inputs. The result reshaped the architecture of every major package manager. OpenSUSE's libsolv (used by zypper, dnf, microdnf), Fedora's dnf, the original libapt — all run a SAT solver internally. Apt uses a heuristic scoring approach, which is why it occasionally proposes removing your desktop environment. npm and Cargo make pragmatic compromises that avoid SAT but accept incompatible-version trees.
Mancinelli, F., Boender, J., Di Cosmo, R., Vouillon, J., Durak, B., Leroy, X., Treinen, R. (2006). Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, 199–208. Source → 🇫🇷 Cultural context · France
Mid-2000s France was investing in academic open-source research at scale, partly as European pushback against US dominance of the software industry. Debian and the broader Linux distribution ecosystem were maturing into the infrastructure of the modern internet. The EU-funded EDOS project (Environment for the Development and Distribution of Open Source software) was the political vehicle for the work. Di Cosmo combined formal verification expertise with practical Debian-developer experience — a rare combination — and the result was the first proof of NP-completeness for an everyday system tool. The architecture of package managers has been shaped by this paper ever since.
In plain terms
Most developers think of package management as boring infrastructure. You type apt install or npm install and the right thing happens. Sometimes the wrong thing happens — a package gets removed that you wanted, or a version conflict makes the install fail. When that happens you blame the tool.
The tool is doing the best it can with an NP-complete problem.
A real package repository is a giant constraint satisfaction problem. Every package declares dependencies (I need libfoo ≥ 2.1) and conflicts (I cannot coexist with libfoo < 2.0 or libbar 3.x). When you ask for a set of packages to be installed, the package manager has to find a complete assignment — a specific version of every transitive dependency — that satisfies all the constraints simultaneously. Di Cosmo's reduction shows this is exactly 3-SAT.
This is not theoretical. In 2005 Di Cosmo and colleagues constructed real Debian package configurations that caused dpkg to spend minutes — sometimes hours — looking for a satisfying assignment. And these were not adversarial inputs cooked up in a lab. They were real-world repositories at the scale Debian was already operating.
The response was architectural. OpenSUSE built libsolv, an actual SAT solver inside the package manager. Fedora's dnf uses libsolv. The Maven dependency mediator switched to SAT. Eclipse's P2 update manager runs a SAT solver internally. When you install software on a modern Linux system, you are running a 3-SAT solver and you do not know it.
Apt took the other path. Apt does not run a real SAT solver — it runs a greedy scoring heuristic that picks the first satisfying assignment it finds. This is why apt occasionally suggests "the following packages will be REMOVED" with a list that includes half your desktop. The scoring heuristic gave up and proposed an extreme solution because the problem was, in that instance, hard.
npm v7+ and Cargo make a different compromise. Instead of finding one global assignment, they let different parts of the dependency tree have different versions of the same package. This avoids the SAT problem entirely by relaxing the constraints — but at the cost of pulling multiple versions of the same library into your build. This is the reason node_modules is enormous.
Every time you install a package, you are running an NP-complete problem. The problem has not gotten easier in twenty years. Only the heuristics have.
Your package manager is a SAT solver. It has to be.