Begriff
SAT Solver
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Wir wissen: SAT (Erfüllbarkeitsproblem der Aussagenlogik) ist NP-Complete. Also theoretisch unlösbar für große Fälle. Aber in der Praxis? Wir haben Solver gebaut (MiniSat, Glucose, Kissat), die Problemen mit Millionen von Variablen lösen können. Wie? Sie sind extrem schlau beim Raten. Statt alle $2^N$ Möglichkeiten zu probieren, lernen sie aus Fehlern ("Conflict Driven Clause Learning"). SAT Solver sind der Motor der modernen Verifikation.
Merksatz: Ein Algorithmus oder Software-Tool, das das Erfüllbarkeitsproblem der Aussagenlogik (SAT) löst, indem es entscheidet, ob eine Belegung von Variablen existiert, die eine gegebene boolesche Formel wahr macht.
- Dependency Management:
npm installoderapt-getnutzen SAT Solver. "Ich will Paket A v2.0. A braucht B v1.0. C braucht B v2.0. Geht das?" Der Solver sagt: "Konflikt! Unmöglich." - Hardware Design: Intel nutzt SAT, um Schaltkreise zu prüfen.
- Terminplanung: "Finde einen Plan für 1000 Züge ohne Kollision."
1. CDCL (Conflict-Driven Clause Learning)
Der Algorithmus, der alles verändert hat.
Der Solver rät: x1 = True.
Er läuft in einen Widerspruch (Konflikt).
Er analysiert den Konflikt und lernt eine neue Regel (Clause), die diesen Fehler in Zukunft verbietet.
"Aha, x1=True und x5=False geht niemals zusammen."
Er fügt die Regel zur Datenbank hinzu.
Er wird schlauer, je länger er läuft.
2. SMT (Satisfiability Modulo Theories)
SAT kann nur True/False.
SMT (wie Z3) kann auch Zahlen (x > 5), Arrays und Strings.
SMT Solver nutzen SAT Solver als Kern ("Bit-Blasting"), sind aber viel mächtiger für Software.
1. VSIDS (Variable State Independent Decaying Sum)
Die Magie des Ratens. Wie entscheidet der Solver, welche Variable er als nächstes prüft? VSIDS ist eine Heuristik: Jedes Mal, wenn eine Variable an einem Konflikt beteiligt ist, steigt ihre Priorität. Aber: Über Zeit sinken alle Prioritäten langsam ab (Decay). Das Ergebnis: Der Solver konzentriert sich "heiß" auf den Bereich der Formel, der gerade Probleme macht. Sobald dieser gelöst ist, "vergisst" er ihn und zieht weiter zum nächsten Problembereich. Das macht den Solver adaptiv und ist der Grund für den exponentiellen Speedup seit den 2000ern.
2. Luby Restarts & Phase Saving
SAT Solver geben niemals auf, aber sie "starten neu".
Wenn der Solver merkt, dass er sich verrannt hat, bricht er die aktuelle Suche ab (Restart) und fängt bei den Variablen ganz oben neu an – aber er behält sein gelerntes Wissen (Learned Clauses).
Mit Phase Saving merkt er sich zudem, welche Logik-Belegung (True oder False) zuletzt am besten funktioniert hat. Beim Neustart nutzt er diese Belegung sofort wieder. Das verhindert, dass der Solver ewig im "falschen" Teil des Suchraums stagniert.
3. Symmetry Breaking & Preprocessing
Viele Probleme (z.B. das Verschieben von 10 identischen Containern) haben Symmetrien. Der Solver würde 10! (Millionen) identische Wege probieren. Experten nutzen Symmetry Breaking Constraints: Man fügt Regeln hinzu, die sagen: "Behandle Container 1 immer wie Container 2, außer wenn...". Zusammen mit Preprocessing (Techniken wie Variable Elimination oder Subsumption) wird die Formel massiv geschrumpft, bevor die erste Variable überhaupt geraten wird. Ein gut konfigurierter Preprocessor kann die Problemgröße oft um 50-80% reduzieren.
Quick-Check
Gewinnt er immer?
Nein. Manchmal läuft er ewig. Aber für "industrielle Instanzen" (echte Probleme) funktioniert er erstaunlich oft in Millisekunden.Input Format?
DIMACS CNF. Eine Textdatei mit Zahlen.1 -2 0heißtx1 OR NOT x2. Sehr unlesbar, aber Standard.Wettbewerbe?
SAT Competition. Jedes Jahr treten die besten Solver der Welt gegeneinander an. Die Performance steigt schneller als Moore's Law.