Case Study: How Debian’s Solver Works

Updated

October 30, 2026

Case Study: How Debian’s Solver Works

Debian’s package ecosystem is one of the largest in the world, maintaining over 60,000 binary packages across more than 10 CPU architectures. Managing dependencies across this colossal universe requires deep mathematical algorithms.

+-----------------------------------------------------------+
|                   Debian's Dual-Solver Engine             |
|                                                           |
|  User Request: `apt-get install nginx`                    |
|         |                                                 |
|         +---> Internal Solver (libapt-pkg)                |
|         |     - Fast heuristic graph traversal            |
|         |     - Resolves 98% of everyday operations       |
|         |                                                 |
|         +---> External EDSP Solvers (aspcud / dose3)      |
|               - Invoked on complex dist-upgrades          |
|               - Translates universe to MaxSAT problem     |
|               - Optimizes criteria: minimize removals     |
+-----------------------------------------------------------+

The Internal libapt-pkg Heuristic Solver

For everyday installations, apt employs an internal heuristic solver based on depth-first search with backtracking. - It calculates an urgency score for packages based on whether they are marked as essential, whether they satisfy a direct user request, or whether they resolve an immediate breakage. - While fast, the internal heuristic solver is not complete: in rare scenarios with conflicting multi-version upgrades, it can make suboptimal choices or propose removing packages unnecessarily.

The External Solver Protocol (EDSP)

To solve complex distribution-wide upgrades (e.g., upgrading from Debian 11 Bullseye to Debian 12 Bookworm), Debian architects developed the External Dependency Solver Protocol (EDSP).

When invoked with --solver, apt dumps the entire state of the package universe (installed packages, available candidates, version constraints, preferences) into a standardized plaintext stream and pipes it to an external solver:

# Excerpt from EDSP dump:
Request: EDSP 0.5
Architecture: amd64
Install: nginx
Strict-Pinning: yes

Package: nginx
Version: 1.22.1-9
Architecture: amd64
Depends: nginx-core (>= 1.22.1-9) | nginx-full (>= 1.22.1-9)

SAT and MaxSAT: Optimizing Upgrade Criteria

External solvers like aspcud (Answer Set Programming) convert the EDSP problem into a MaxSAT (Maximum Satisfiability) optimization problem.

Instead of merely finding any valid installation state, MaxSAT optimizes a multi-objective cost function: 1. Rule 1 (Strict): No conflicting packages may be installed simultaneously. 2. Rule 2 (Strict): Every dependency of an installed package must be satisfied. 3. Objective 1 (Minimize): Minimize the number of removed packages. 4. Objective 2 (Maximize): Maximize the number of upgraded packages. 5. Objective 3 (Minimize): Minimize the total download footprint.

The solver runs a mathematical branch-and-bound optimization, guaranteeing the most elegant, non-destructive upgrade path possible.