Wie CDCL funktioniert — und wie man misst, ohne sich zu täuschen

Was ein SAT-Löser gefragt wird

Eine Formel in konjunktiver Normalform ist eine Liste von Klauseln; eine Klausel ist eine Liste von Literalen, jedes eine Variable oder ihre Negation. Die Formel ist erfüllt, wenn in jeder Klausel mindestens ein Literal wahr ist. Gefragt ist, ob es eine solche Belegung gibt.

Eine Regel leistet in der Praxis fast die ganze Arbeit: die Einheitspropagation. Sind in einer Klausel alle Literale bis auf eines falsch, muss das letzte wahr sein. Eine gesetzte Variable kann eine zweite erzwingen, die eine dritte erzwingt — eine Kettenreaktion, deren Verfolgung nichts kostet.

DPLL: raten, propagieren, zurücknehmen

Das klassische Verfahren (Davis–Putnam–Logemann–Loveland, 1962) wiederholt drei Schritte: eine unbelegte Variable wählen und einen Wert raten, propagieren, und wenn eine Klausel nur noch falsche Literale hat — ein Konflikt —, die letzte Vermutung zurücknehmen und den anderen Wert probieren. Dieses Zurücknehmen nur der jüngsten Vermutung heisst chronologisches Backtracking.

Seine Schwäche: Der Grund eines Konflikts liegt oft mehrere Vermutungen zurück. DPLL weiss das nicht und findet denselben Konflikt in jedem Zweig unterhalb der Vermutung, die ihn wirklich verursacht hat, neu.

CDCL: aus jedem Konflikt lernen

Conflict-Driven Clause Learning behält die Schleife von DPLL und fügt ein Gedächtnis hinzu. Die Bausteine:

1 · Der Implikationsgraph. Jedes propagierte Literal merkt sich die Klausel, die es erzwungen hat — seinen Grund. Tritt ein Konflikt auf, bilden diese Gründe einen Graphen zurück zu den verantwortlichen Vermutungen.

2 · Konfliktanalyse (1UIP). Beginne mit der Konfliktklausel und resolviere sie wiederholt mit dem Grund ihres zuletzt belegten Literals. Resolution fasst zwei Klauseln, die sich in einer Variablen widersprechen, zu einer Klausel zusammen, die aus beiden folgt — das Ergebnis folgt also aus der Formel und darf hinzugefügt werden. Halte an, sobald nur noch ein Literal der aktuellen Entscheidungsebene übrig ist: der erste eindeutige Implikationspunkt. Die gefundene Klausel ist die gelernte Klausel.

3 · Nicht-chronologischer Rücksprung. Springe auf die zweithöchste Entscheidungsebene unter den Literalen der gelernten Klausel zurück. Dort hat die gelernte Klausel genau ein unbelegtes Literal, und die Propagation erzwingt sofort die andere Richtung. Vermutungen, die mit dem Konflikt nichts zu tun hatten, werden übersprungen.

4 · VSIDS. Variablen, die in jüngsten Konflikten vorkommen, bekommen einen höheren Punktwert; alle Werte verfallen mit der Zeit. Der Löser rät auf dem höchsten Wert — er arbeitet dort weiter, wo die Konflikte sind.

5 · Neustarts, Phasenspeicher, Klausellöschung. Gelegentlich alle Vermutungen verwerfen, gelernte Klauseln und Punktwerte aber behalten (Neustart); beim erneuten Raten einer Variablen ihren letzten Wert nehmen (Phasenspeicher); regelmässig gelernte Klauseln löschen, die nutzlos aussehen, gemessen daran, über wie viele Entscheidungsebenen sie reichen (LBD).

6 · Beobachtete Literale. Jede Klausel beobachtet zwei ihrer Literale und wird nur angesehen, wenn eines davon falsch wird. Das macht Propagation billig genug für Millionen Schritte je Sekunde.

Ein Lauf, Schritt für Schritt

Eine kleine unerfüllbare Formel mit 5 Variablen und 10 Klauseln. Der Löser rät die kleinste unbelegte Variable und probiert zuerst falsch. Der Lauf stammt aus einem protokollierenden Löser (lehrseite/mini_cdcl.py), der auf 3 000 Zufallsformeln mit Brute Force übereinstimmt.

Die Analyse in Schritt 7. Drei Vermutungen sind gefallen; auf Ebene 3 hat die Propagation zwei Literale erzwungen, und Klausel c3 ist falsch geworden. Rückwärts durch die Gründe resolviert:

Start mit der Konfliktklausel              (x3 ∨ x4 ∨ ¬x5)
auflösen nach x5 mit Grund c2 (x3 ∨ x5)      →  (x3 ∨ x4)
auflösen nach x4 mit Grund c1 (x3 ∨ ¬x4)     →  (x3)
nur noch ein Literal der aktuellen Ebene übrig: das ist die 1UIP-Klausel

Die gelernte Klausel ist (x3) — ein einziges Literal. Keine der ersten beiden Vermutungen spielte eine Rolle, also springt der Löser von Ebene 3 direkt auf Ebene 0 und setzt x3 endgültig. Auf Ebene 0 läuft jetzt schon die Propagation allein in einen Konflikt: Die Formel ist unerfüllbar, bewiesen mit einer gelernten Klausel. DPLL, das eine Vermutung nach der anderen zurücknimmt, hätte zuerst noch die Vermutungen auf Ebene 2 und 1 durchprobiert.

Was jeder Baustein einbringt — gemessen

Aus der Ablation in diesem Projekt: der Haus-CDCL-Löser mit einzeln abgeschalteten Bausteinen, auf je 150 unerfüllbaren Zufalls-3-SAT-Instanzen an der Schwelle. Median der Konflikte je Instanz (Median über 21 Saaten; beim reinen Backtracking über 41).

Auf diesen Instanzen bringt der Phasenspeicher nichts und bringen Neustarts wenig. Lernen und adaptive Verzweigung bringen jeweils etwa Faktor 4 bei n = 100 und 7–9 bei n = 130; beide wegzunehmen kostet etwa Faktor 80. Die beiden sind weitgehend redundant — jeder allein holt den grössten Teil zurück. Auf industriellen Instanzen sieht das anders aus; das hier ist eine Familie in zwei Grössen.

Nullmessungen: wie eine Zahl aussieht, wenn nichts da ist

Jede Messung mischt das Signal mit Rauschen, Auswahl und den Eigenheiten des Messverfahrens. Eine Nullmessung fährt die komplette Auswertung an einem Fall, bei dem der wahre Effekt bekannt null ist, und zeigt, wie gross ein „Effekt" ist, den die Auswertung von selbst erzeugt. Nur was klar darüber liegt, ist ein Befund.

Jede der folgenden Regeln hat in diesem Projekt ein konkretes falsches Ergebnis aufgehalten.

Im Programmieralltag

Nichts davon braucht Statistiksoftware. Es braucht eine Gewohnheit.

1 · Bevor man einer Beschleunigung glaubt: A gegen A messen

Den alten Code mit demselben Messaufbau gegen sich selbst laufen lassen. Die Streuung, die man dann sieht, ist das Aussehen von „keine Änderung". Eine neue Fassung gilt nur als schneller, wenn sie klar ausserhalb dieser Streuung landet. Die Läufe abwechseln (alt, neu, alt, neu), damit Hintergrundlast beide gleich trifft, und Mediane nehmen.

import statistics, time

def laufzeit(f, x):
    t = time.perf_counter(); f(x); return time.perf_counter() - t

def verhaeltnisse(alt, neu, eingaben, runden=15):
    """Je Eingabe: Median(neu) / Median(alt), abwechselnd gemessen."""
    aus = []
    for x in eingaben:
        a, b = [], []
        for _ in range(runden):
            a.append(laufzeit(alt, x))
            b.append(laufzeit(neu, x))        # abwechselnd, nicht erst alle alten
        aus.append(statistics.median(b) / statistics.median(a))
    return aus

null = verhaeltnisse(sortiere, sortiere, eingaben)       # A gegen A: kein echter Unterschied
echt = verhaeltnisse(sortiere, sortiere_neu, eingaben)   # A gegen B
print("so viel 'Effekt' macht das Rauschen:", min(null), "bis", max(null))
print("gemessener Effekt:", statistics.median(echt))

2 · Eine Antwort darf nicht an Namen hängen

Ids mischen, Eingaben umordnen, Schlüssel umbenennen — alles, was keine Rolle spielen sollte. Ändert sich das Ergebnis, ist es ein Fehler. Ändert sich die Laufzeit stark, misst der Benchmark Gleichstandsregeln und Hash-Reihenfolge, nicht den Algorithmus.

import random

def test_ergebnis_haengt_nicht_an_namen(algo, graph, versuche=50):
    erwartet = algo(graph)
    for _ in range(versuche):
        neu = list(graph.knoten); random.shuffle(neu)
        umbenannt = graph.umbenennen(dict(zip(graph.knoten, neu)))
        # gilt fuer Ergebnisse, die selbst keine Namen enthalten (Anzahl, Laenge, ja/nein);
        # sonst das Ergebnis vorher zurueckuebersetzen
        assert algo(umbenannt) == erwartet     # die Antwort darf nicht an Namen haengen
        # und wenn die LAUFZEIT stark schwankt: dann misst man Gleichstandsregeln,
        # nicht die Eingabe -- vor jedem Benchmark wissen

3 · Positivkontrollen: findet der Code, was bekannt da ist?

Gegen Brute Force auf kleinen Eingaben testen, und gegen Eingaben mit eingebauter Antwort. Eine Testsuite, die nur „keine Ausnahme" prüft, ist eine Sonde ohne Positivkontrolle.

# Positivkontrolle 1: gegen Brute Force auf kleinen Eingaben
for _ in range(10_000):
    x = kleine_zufallseingabe()
    assert schnell(x) == brute_force(x), x

# Positivkontrolle 2: eine Eingabe mit bekannter, eingebauter Antwort
x, antwort = eingabe_mit_gepflanzter_loesung()
assert schnell(x) == antwort

4 · Ablation statt Raten, welcher Teil hilft

Besteht eine Optimierung aus mehreren Ideen, jede hinter einen Schalter legen. Zuerst prüfen, dass alle Schalter an exakt das alte Verhalten liefern. Dann einen nach dem anderen ausschalten. Regelmässig stellt sich heraus, dass eine Idee alles trägt und eine andere nichts — oder dass zwei redundant sind, wie oben Lernen und VSIDS.

from dataclasses import dataclass, replace

@dataclass(frozen=True)
class Schalter:
    cache: bool = True
    fruehabbruch: bool = True
    heuristik: bool = True

def algo(x, s=Schalter()):
    ...

# 1. Voreinstellung muss exakt das alte Verhalten liefern (sonst misst man den Umbau)
assert all(algo(x) == algo_vorher(x) for x in testfaelle)

# 2. je einen Baustein herausnehmen und gegen die volle Fassung messen
for name in ("cache", "fruehabbruch", "heuristik"):
    ohne = replace(Schalter(), **{name: False})
    print(name, statistics.median(verhaeltnisse(algo, lambda x: algo(x, ohne), eingaben)))

5 · Regression zur Mitte bei Performance-Arbeit

„Meine Änderung hat den langsamsten Benchmarks am meisten geholfen" sieht man auch ohne Änderung: Die Fälle, die in einer Messung am langsamsten waren, sind in der nächsten im Mittel weniger langsam. Vor diesem Schluss den unveränderten Code erneut messen und dieselbe Grafik ansehen.

6 · Die beste von fünfzig Einstellungen ist zu optimistisch

Einen Parameter auf einer Benchmark-Menge einstellen und den besten Wert berichten überschätzt den Gewinn, weil das Maximum verrauschter Zahlen nach oben verzerrt ist. Auf einer Menge wählen, auf einer anderen berichten.