solver3.md

subject	title	subtitle	documentclass	classoption	secnumdepth	toc-depth	header-includes	links-as-notes	toc	listings	highlight-style	author	reference-section-title	biblio-title
Dependency solving	APT 3.0 dependency solver	An orthodox approach to dependency solving, leading to a SAT solver comparable to DPLL.	scrartcl	BCOR=0.5cm	2	1	\usepackage[]{graphicx} \usepackage[english]{babel}	true	true	true	monochrome - \fontfamily{lmvtt}\selectfont	Julian Andres Klode \  \ Canonical Ltd	References	References,heading=bibintoc

Introduction

Definitions

Facts

Let

• $\mathcal{V}$ be the set of versions in the apt cache (literals)
• $\mathcal{I} \subset{\mathcal{V}}$ be the set of installed versions
• $\mathcal{M} \subset{\mathcal{I}}$ be the set of manually installed versions
• $\mathcal{A} = \mathcal{I} \setminus \mathcal{M}$ be the set of automatically installed versions

Let

• $\mathcal{D}_{V} \subset {D1 \vee \ldots \vee D_n \mid D_1, \ldots, D_n \in \mathcal{V} }$
• $\mathcal{C}_{V} \subset {C \mid C \in \mathcal{V} }$

denote the dependencies and conflicts of $V \in \mathcal{V}$. These correspond to the formulas: $V \rightarrow D1 \vee \ldots \vee D_n$ and $V \rightarrow \neg{C}$.

(TODO: Optional dependencies)

Let $|D_1\vee \ldots \vee D_n|=n$ represent the number of choices in a given "or group".

Solver state

For depth $i \in \mathbb{N}$, and step $j \in \mathbb{N}$:

Let

• ${needs}_{ij} \subset \mathcal{V}$ denote the set of versions that shall be installed
• ${rejects}_{ij} \subset \mathcal{V}$ denote the set of versions that shall not be installed
• ${wants}_ij \subset \mathcal{V}$ denote the set of versions that we want installed later (optional dependencies)
• ${likes}_{ij} \subset \mathcal{V}$ denote the set of versions that are also suggested by packages (more optional)

Let $allversions(V)$ denote the ordered set of all (allowed for install) versions of the package that V is a version of.

Let ${work}_{ij} \subset { V \rightarrow D \mid D \in \mathcal{D}{V} }$ denote the work queue of unsatisfied dependencies.

Let ${needs}{00} = {rejects}{00} = {wants}{00} = likes{00} = \emptyset$.

Iteration

Let the symbol $\bot$ determine termination of the solver (mostly fatal), and $\top$ denote termination of that level.

\begin{align*} {needs}{i,j+1} &= \begin{cases} \bot & \text{if } \forall d \in w: d \in {rejects}{ij} \ {needs}{ij} & \text{if } \exists d \in w: d \in {needs}{ij} \text{ (already installed) } \ {needs}{ij} \cup {d} & \text{if } \exists d \in w: d = {w} \text{ (single choice)}\ \top & \text{ otherwise } \end{cases} \ {rejects}{i,j+1} &= \begin{cases} \bot & \text{if } {needs}{i,j+1} = \bot \ \top & \text{if } {needs}{i,j+1} = \top \ {rejects}_{ij} \cup { d \in \mathcal{C}_d } & \text{otherwise} \ \end{cases} \end{align*}