Created
July 10, 2023 17:14
-
-
Save julian-klode/8e2669ee40ca7ae73f6d177e563c2683 to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang=""> | |
| <head> | |
| <meta charset="utf-8" /> | |
| <meta name="generator" content="pandoc" /> | |
| <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" /> | |
| <title>APT 3.0 dependency solver</title> | |
| <style> | |
| html { | |
| line-height: 1.5; | |
| font-family: Georgia, serif; | |
| font-size: 20px; | |
| color: #1a1a1a; | |
| background-color: #fdfdfd; | |
| } | |
| body { | |
| margin: 0 auto; | |
| max-width: 36em; | |
| padding-left: 50px; | |
| padding-right: 50px; | |
| padding-top: 50px; | |
| padding-bottom: 50px; | |
| hyphens: auto; | |
| overflow-wrap: break-word; | |
| text-rendering: optimizeLegibility; | |
| font-kerning: normal; | |
| } | |
| @media (max-width: 600px) { | |
| body { | |
| font-size: 0.9em; | |
| padding: 1em; | |
| } | |
| h1 { | |
| font-size: 1.8em; | |
| } | |
| } | |
| @media print { | |
| body { | |
| background-color: transparent; | |
| color: black; | |
| font-size: 12pt; | |
| } | |
| p, h2, h3 { | |
| orphans: 3; | |
| widows: 3; | |
| } | |
| h2, h3, h4 { | |
| page-break-after: avoid; | |
| } | |
| } | |
| p { | |
| margin: 1em 0; | |
| } | |
| a { | |
| color: #1a1a1a; | |
| } | |
| a:visited { | |
| color: #1a1a1a; | |
| } | |
| img { | |
| max-width: 100%; | |
| } | |
| h1, h2, h3, h4, h5, h6 { | |
| margin-top: 1.4em; | |
| } | |
| h5, h6 { | |
| font-size: 1em; | |
| font-style: italic; | |
| } | |
| h6 { | |
| font-weight: normal; | |
| } | |
| ol, ul { | |
| padding-left: 1.7em; | |
| margin-top: 1em; | |
| } | |
| li > ol, li > ul { | |
| margin-top: 0; | |
| } | |
| blockquote { | |
| margin: 1em 0 1em 1.7em; | |
| padding-left: 1em; | |
| border-left: 2px solid #e6e6e6; | |
| color: #606060; | |
| } | |
| code { | |
| font-family: Menlo, Monaco, 'Lucida Console', Consolas, monospace; | |
| font-size: 85%; | |
| margin: 0; | |
| } | |
| pre { | |
| margin: 1em 0; | |
| overflow: auto; | |
| } | |
| pre code { | |
| padding: 0; | |
| overflow: visible; | |
| overflow-wrap: normal; | |
| } | |
| .sourceCode { | |
| background-color: transparent; | |
| overflow: visible; | |
| } | |
| hr { | |
| background-color: #1a1a1a; | |
| border: none; | |
| height: 1px; | |
| margin: 1em 0; | |
| } | |
| table { | |
| margin: 1em 0; | |
| border-collapse: collapse; | |
| width: 100%; | |
| overflow-x: auto; | |
| display: block; | |
| font-variant-numeric: lining-nums tabular-nums; | |
| } | |
| table caption { | |
| margin-bottom: 0.75em; | |
| } | |
| tbody { | |
| margin-top: 0.5em; | |
| border-top: 1px solid #1a1a1a; | |
| border-bottom: 1px solid #1a1a1a; | |
| } | |
| th { | |
| border-top: 1px solid #1a1a1a; | |
| padding: 0.25em 0.5em 0.25em 0.5em; | |
| } | |
| td { | |
| padding: 0.125em 0.5em 0.25em 0.5em; | |
| } | |
| header { | |
| margin-bottom: 4em; | |
| text-align: center; | |
| } | |
| #TOC li { | |
| list-style: none; | |
| } | |
| #TOC ul { | |
| padding-left: 1.3em; | |
| } | |
| #TOC > ul { | |
| padding-left: 0; | |
| } | |
| #TOC a:not(:hover) { | |
| text-decoration: none; | |
| } | |
| code{white-space: pre-wrap;} | |
| span.smallcaps{font-variant: small-caps;} | |
| span.underline{text-decoration: underline;} | |
| div.column{display: inline-block; vertical-align: top; width: 50%;} | |
| div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;} | |
| ul.task-list{list-style: none;} | |
| .display.math{display: block; text-align: center; margin: 0.5rem auto;} | |
| </style> | |
| </head> | |
| <body> | |
| <header id="title-block-header"> | |
| <h1 class="title"><p>APT 3.0 dependency solver</p></h1> | |
| <p class="subtitle"><p>An orthodox approach to dependency solving, | |
| leading to a SAT solver comparable to DPLL.</p></p> | |
| <p class="author"><p>Julian Andres Klode<br /> | |
| Β <br /> | |
| Canonical Ltd</p></p> | |
| </header> | |
| <nav id="TOC" role="doc-toc"> | |
| </nav> | |
| <h1 id="introduction">Introduction</h1> | |
| <h1 id="definitions">Definitions</h1> | |
| <h2 id="facts">Facts</h2> | |
| <p>Let</p> | |
| <ul> | |
| <li><span class="math inline">π±</span> be the set of versions in the apt | |
| cache (literals)</li> | |
| <li><span class="math inline">ββββπ±</span> be the set of installed | |
| versions</li> | |
| <li><span class="math inline">β³ββββ</span> be the set of manually | |
| installed versions</li> | |
| <li><span class="math inline">πβ=βββ \β β³</span> be the set of | |
| automatically installed versions</li> | |
| </ul> | |
| <p>Let</p> | |
| <ul> | |
| <li><span | |
| class="math inline">π<sub><em>V</em></sub>βββ{<em>D</em>1β β¨β β¦β β¨β <em>D</em><sub><em>n</em></sub>β β£β <em>D</em><sub>1</sub>,ββ¦,β<em>D</em><sub><em>n</em></sub>βββπ±}</span></li> | |
| <li><span | |
| class="math inline">π<sub><em>V</em></sub>βββ{<em>C</em>β β£β <em>C</em>βββπ±}</span></li> | |
| </ul> | |
| <p>denote the dependencies and conflicts of <span | |
| class="math inline"><em>V</em>βββπ±</span>. These correspond to the | |
| formulas: <span | |
| class="math inline"><em>V</em>βββ<em>D</em>1β β¨β β¦β β¨β <em>D</em><sub><em>n</em></sub></span> | |
| and <span class="math inline"><em>V</em>βββΒ¬<em>C</em></span>.</p> | |
| <p>(TODO: Optional dependencies)</p> | |
| <p>Let <span | |
| class="math inline">|<em>D</em><sub>1</sub>β¨β¦β¨<em>D</em><sub><em>n</em></sub>|β=β<em>n</em></span> | |
| represent the number of choices in a given βor groupβ.</p> | |
| <h2 id="solver-state">Solver state</h2> | |
| <p>For depth <span class="math inline"><em>i</em>ββββ</span>, and step | |
| <span class="math inline"><em>j</em>ββββ</span>:</p> | |
| <p>Let</p> | |
| <ul> | |
| <li><span | |
| class="math inline"><em>n</em><em>e</em><em>e</em><em>d</em><em>s</em><sub><em>i</em><em>j</em></sub>βββπ±</span> | |
| denote the set of versions that shall be installed</li> | |
| <li><span | |
| class="math inline"><em>r</em><em>e</em><em>j</em><em>e</em><em>c</em><em>t</em><em>s</em><sub><em>i</em><em>j</em></sub>βββπ±</span> | |
| denote the set of versions that shall not be installed</li> | |
| <li><span | |
| class="math inline"><em>w</em><em>a</em><em>n</em><em>t</em><em>s</em><sub><em>i</em></sub><em>j</em>βββπ±</span> | |
| denote the set of versions that we want installed later (optional | |
| dependencies)</li> | |
| <li><span | |
| class="math inline"><em>l</em><em>i</em><em>k</em><em>e</em><em>s</em><sub><em>i</em><em>j</em></sub>βββπ±</span> | |
| denote the set of versions that are also suggested by packages (more | |
| optional)</li> | |
| </ul> | |
| <p>Let <span | |
| class="math inline"><em>a</em><em>l</em><em>l</em><em>v</em><em>e</em><em>r</em><em>s</em><em>i</em><em>o</em><em>n</em><em>s</em>(<em>V</em>)</span> | |
| denote the ordered set of all (allowed for install) versions of the | |
| package that V is a version of.</p> | |
| <p>Let <span | |
| class="math inline"><em>w</em><em>o</em><em>r</em><em>k</em><sub><em>i</em><em>j</em></sub>βββ{<em>V</em>βββ<em>D</em>β β£β <em>D</em>βββπ<em>V</em>}</span> | |
| denote the work queue of unsatisfied dependencies.</p> | |
| <p>Let <span | |
| class="math inline"><em>n</em><em>e</em><em>e</em><em>d</em><em>s</em><sub>00</sub>β=β<em>r</em><em>e</em><em>j</em><em>e</em><em>c</em><em>t</em><em>s</em><sub>00</sub>β=β<em>w</em><em>a</em><em>n</em><em>t</em><em>s</em><sub>00</sub>β=β<em>l</em><em>i</em><em>k</em><em>e</em><em>s</em><sub>00</sub>β=ββ </span>.</p> | |
| <h2 id="iteration">Iteration</h2> | |
| <p>Let the symbol <span class="math inline">β₯</span> determine | |
| termination of the solver (mostly fatal), and <span | |
| class="math inline">β€</span> denote termination of that level.</p> | |
| <p></p> | |
| </body> | |
| </html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment