Paketverwaltung/SAT Solver/Grundlagen

aus openSUSE, der freien Wissensdatenbank

Grundlagen von SAT Solver

Basierend auf einer von Michael Schröder auf dem FOSDEM 2008 gegebenen Präsentation.

Das SAT-Problem

• SAT: Erfüllbarkeitsproblem der Aussagenlogik (SAT, von engl. satisfiability)

finde eine True/False-Zuweisung zu allen Variablen eines boolschen Ausdrucks (AND/OR/NOT), so dass es True ist. NP-Vollständigkeit

• Normalisierung:

(a | b | c) & (d | e | f) ... = TRUE

Die (...) Bedingungen nennt man aus Literale bestehende Regeln a, b, c kann außerdem negiert werden: -a

Beispiel:

(a | b | c) & (-c) & (-a | c) = TRUE

Lösung: a = FALSE, b = TRUE, c = FALSE

Vorteile von SAT

• Gut untersuchtes Problem
  • Es sind viele Beispiel-Sovler verfügbar (chaff, minisat...)
• Sehr schnell
  • Die Komplexität von Paketabhängigkeiten ist im Vergleich zu anderen Einsatzgebieten von SAT sehr gering
• Keine komplexen Algorithmen
  • Das Auflösen braucht nur ein paar Hundert Zeilen Code
• Verständliche Vorschläge
  • Der Solver kalkuliert Nachweise, warum ein Problem nicht lösbar ist

Von Abhängigkeiten zu Regeln

Requires: package Abhängigkeiten

A benötigt B, welches von B1, B2, B3 angeboten wird
Regel: (-A | B1 | B2 | B3)

“entweder ist A nicht installiert, oder keins von B1, B2, B3 ist installiert”

Conflicts: package Abhängigkeiten

A steht im Konflikt zu B, welches von B1, B2, B3 angeboten wird
3 Regeln: (-A | -B1), (-A | -B2), (-A | -B3)

“entweder ist A nicht installiert, oder B1 ist nicht installiert”

Obsoletes: package Abhängigkeiten

Wird wie Conflicts behandelt

Mehr zum Erstellen von Regeln

Solver-Algorithmus

Unit Propagation

Eine Regel wird Klausel (unit) genannt, wenn alle Literale bis auf einen FALSE sind
Wenn eine Regel eine Klausel ist, können die verbliebenen Literale auf TRUE gesetzt werden Beispiel:

(a | b | c) & (-c) & (-a | c) = TRUE
c ist FALSE     (Unäre Regel)
(-a | c) ist eine Einheit → -a ist TRUE, a ist FALSE
(a | b | c) ist eine Einheit → b ist TRUE

Algorithmus

1. freie Auswahl: finde einige unbestimmte Variablen, weise TRUE oder FALSE zu
2. propagate all unit rules
3. Wiederhole die Klausel bis alle Variablen gesetzt sind

Unit Propagation & Abhängigkeiten

Requires-Klausel (-A | B1 | B2 | B3)

• A, B1, B2 ist FALSE → B3 muss TRUE sein
  • “Wenn A installiert ist und alle bis auf einen Anbieter einer Abhängigkeit nicht installiert werden können, muss der verbliebene Anbieter installiert werden”
  • → fügt Pakete dem Installationssatz hinzu
• B1, B2, B3 ist FALSE → A muss FALSE sein
  • “Wenn keiner der Anbieter einer benötigten Abhängigkeit installiert werden kann, kann das anfordernde Paket nicht installiert werden”
  • → fügt ein Paket dem Satz Konflikt/Löschen hinzu

Conflicts-Klausel (-A | -B1)

• A ist TRUE → B1 muss FALSE sein und andersherum

Widersprüche

Unit Propagation kann zu einem Widerspruch führen
Das heißt, dass ein Literal sowohl TRUE als auch FALSE sein muss
Beispiel

 (-a | b) & (-a | c) & (-b | -c)

Wenn der Solver a auf TRUE setzt → b, c ist TRUE, c ist FALSE!

• lerne neue Klauseln aus den in den Widerspruch verwickelten Klauseln
  • → erlernte Klausel ist (-a)
  • mache die letzten drei Zuweisungen rückgängig und sete die Auflösung fort
  • wenn nichts rückgängig gemacht werden kann, war das Problem unlösbar

Das erste Mal wurde dies 1996 im GRASP Solver implementiert.

Umgang mit freier Auswahl

Hier können Sie die Qualität der Lösung beeinflussen:

• versuche, installierte Pakete zu behalten
• minimiere die Anzahl der zu installierenden Pakete

Algorithmus

1. wenn ein Paket vorher schon installiert war und nicht im Konfliktsatz ist, installiere es
2. wenn eine Klausel nicht TRUE ist, aber alle der negativen Literale FALSE sind, wähle den besten der nicht gesetzten positiven Literale und installiere das zugehörige Paket
   (-A | B1 | B2) A TRUE → wähle B1 oder B2
3. installiere kein anderes Paket (setze bspw. alle nicht gesetzten Variablen auf FALSE)

Systemrichtlinien

Eine Richtlinienregel definiert, was mit installierten Paketen geschehen soll

• dürfen deinstalliert oder heruntergestuft werden
• dürfen die die Architektur nicht ändern
• dürfen den Anbieter nicht ändern

Regelformat:

(A | A2 | A3 | A4)

A2/A3/A4 sind die erlaubten Aktualisierungskandidaten (gleicher Name mit neuerer Version oder Paket mit passender Obsoletes:-Abhängigkeite)

Konflikte melden

Wenn das Problem unlösbar bleibt, gibt der Solver einen Satz von Regeln aus, der zum Konflikt führte.

Da ein System ohne installierte RPMs konfliktfrei ist, muss der zurückgelieferte Satz von Regeln mindestens eine Job- oder Richtlinienregel enthalten.

Eine mögliche Lösung ist, eine der Regeln zu entfernen, bspw. einen Job zu entfernen (versuche nicht paket 'foo' zu installieren), oder eine eine Richtlinienregel (erlaube die Deinstallation von Paket 'bar')

Vorteil: Nutzer verstehen solche Regeln!

Fazit

Die Nutzung von SAT-Solver-Algorithmen löste viele der Probleme die der alte Solver hatte

• Geschwindigkeit: um Größen schneller
• zuverlässige Ergebnisse
• Erweiterbarkeit: die Implementierung komplexer Abhängigkeiten ist einfach
• vernünftige Fehlerbericht

Wir arbeiten außerdem an einem neuen Paketdepotformat, das dass wesentlich schnellere wörterbuchbasierte SOLV-Format nutzen kann.