Konfliktlernen verständlich erklärt

Eine Planung scheitert, Sie ändern die letzte Entscheidung und stoßen kurz darauf auf dieselbe Wand. Ein Rechenprogramm kann sich merken, warum es scheiterte, und die Wand künftig umgehen. Diese Seite erklärt das an einer Einladungsliste und zeigt ehrlich, wann sich das Merken lohnt und wann nicht. Erst für Einsteiger, dann für Fachleute.

Zuletzt aktualisiert: 11. November 2026

Ein Wort unbekannt? Das Begriffsverzeichnis erklärt es in wenigen Sätzen.

Eine Einladungsliste, die nicht aufgeht

Sie planen eine Feier. Für jede Person entscheiden Sie nur mit Ja oder Nein, ob sie eingeladen wird. Dazu kommen Regeln. Stellen Sie sich diese drei vor:

• Regel 1: Wird Dora eingeladen, wird auch Erwin eingeladen, denn die beiden kommen nur zusammen.
• Regel 2: Wird Dora eingeladen, wird auch Frieda eingeladen, aus demselben Grund.
• Regel 3: Anna, Erwin und Frieda werden nicht alle drei eingeladen: Das Auto, das sie abholt, hat nur Platz für zwei.

Dazu kommen Gustav und Hanna, die mit diesen Regeln nichts zu tun haben. Die Frage lautet: Gibt es eine Auswahl von Ja und Nein für alle sechs, die alle drei Regeln einhält?

Planen ohne Gedächtnis

Ein einfaches Programm geht vor wie Sie am Küchentisch. Es legt eine Einladung nach der anderen fest und prüft nach jeder, was daraus zwingend folgt. Die Reihenfolge ist Anna, Gustav, Hanna, Dora.

Anna, Gustav und Hanna werden eingeladen; daraus folgt nichts. Dann wird Dora eingeladen. Nach Regel 1 und 2 kommen auch Erwin und Frieda. Jetzt wären Anna, Erwin und Frieda alle drei da, und Regel 3 ist verletzt. Das Programm steckt in einer Sackgasse. Jedes solche Auflaufen gegen eine Wand heißt hier ein Fehlschlag.

Das einfache Programm nimmt nun nur die letzte Entscheidung zurück: Dora wird nicht eingeladen. Dann plant es weiter. Es merkt sich nicht, warum es scheiterte. Ändert es später die Antwort für Hanna oder Gustav und lädt Dora wieder ein, steht dieselbe Wand wieder da. Das kann sich mehrfach wiederholen, obwohl Gustav und Hanna mit der Wand nichts zu tun haben.

Aus der Sackgasse eine Regel machen

Ein Programm, das aus der Sackgasse lernt, fragt nach dem Fehlschlag: Welche meiner Entscheidungen haben die Wand gebaut? Es geht die Folgen rückwärts durch. Regel 3 war verletzt, weil Erwin und Frieda kamen. Beide kamen nach Regel 1 und 2, weil Dora kam. Und Regel 3 zählte drei, weil auch Anna kam. Beteiligt sind also Anna und Dora, Gustav und Hanna nicht.

Daraus schreibt das Programm eine neue Regel auf: Anna und Dora werden nicht beide eingeladen. Neu ist an dieser Regel nichts. Sie folgt aus den drei alten und spricht nur aus, was in ihnen schon steckte.

Dann springt das Programm zurück, und zwar bis zu Annas Einladung, nicht nur zu Dora. Der Grund: Dora zurückzunehmen wäre nur der kleine Schritt des einfachen Programms. Die neue Regel zeigt aber, dass Dora nicht in Frage kommt, solange Anna eingeladen ist, egal was dazwischen bei Gustav und Hanna entschieden wurde. Die Entscheidungen für Gustav und Hanna werden deshalb gestrichen und später neu getroffen, nun mit dem Wissen, dass Dora nicht kommt. Anna bleibt eingeladen. Dieses Vorgehen heißt Konfliktlernen; solche Aufgaben heißen SAT-Aufgaben, nach dem englischen Wort für „erfüllbar“.

Woran Sie das im Alltag erkennen

Sie ändern bei einer Planung die letzte Festlegung, und kurz darauf scheitert es an derselben Stelle. Dann hilft die Frage, welche zwei oder drei Festlegungen zusammen die Wand bilden. Halten Sie diese als Regel „nicht zusammen“ fest.

Was das Gedächtnis kostet

Ob sich das lohnt, hat ein Programm zum Ausprobieren im Browser gemessen, das zu dieser Seite gehört, die Demo. Sie zählt nur, wie oft ein Programm in eine Sackgasse läuft, keine Sekunden. Denn jede neue Regel muss gefunden, gespeichert und danach bei jedem Schritt mitgeprüft werden. Ein Fehlschlag kostet das lernende Programm deshalb mehr Arbeit als das einfache Zurückgehen. Wie viel mehr, ist nicht gemessen.

Lohnt sich das? Erst bei größeren Aufgaben

Die Demo vergleicht beide Programme an zufällig gewürfelten Aufgaben dieser Art mit 30 bis 110 Ja-Nein-Entscheidungen. Auf jede Entscheidung kommen dabei gut vier Regeln. Je Größe wurden vorab 20 Aufgaben festgelegt, damit sich jede Messung wiederholen lässt. Verglichen wird der mittlere Wert (Median). Ein Beispiel: Haben drei Aufgaben 3, 6 und 9 Fehlschläge, ist der mittlere Wert 6, die Zahl in der Mitte, wenn man sie ordnet.

• Kleine Aufgaben: Bis 70 Entscheidungen hatte das Gedächtnis keinen klaren Vorteil.
• Ab etwa 90 Entscheidungen: Das einfache Programm hatte mehr als doppelt so viele Fehlschläge wie das lernende, bei 110 etwa dreieinhalbmal so viele.
• Nur für diese Aufgabenart: Die Grenze ist unscharf und verschiebt sich mit anderen Aufgaben. Mit etwas mehr Regeln je Entscheidung kam der Vorteil später, mit genau vier Regeln blieb er aus. Die Einzelheiten stehen im Teil für Fachleute.

Ein Bild für eine Aufgabe, bei der das Gedächtnis lange nicht hilft: Neun Tauben sollen auf acht Löcher verteilt werden, jede in ein eigenes Loch. Das geht nicht, und beim Zählen sehen Sie es sofort. Ein Programm, das Entscheidungen durchprobiert, braucht dafür mit jedem weiteren Loch mehr Fehlschläge. Das Merken von Regeln brachte bis sieben Löcher keinen Vorteil. Warum, hat die Demo nicht untersucht.

Was der Vergleich misst und was nicht

Das lernende Programm unterscheidet sich vom einfachen nicht nur durch das Gedächtnis: Es wählt die nächste Entscheidung nach einer anderen Regel und fängt die Suche nach einer Weile von vorn an. Der Vergleich misst daher den Unterschied beider Programme insgesamt, nicht das Lernen allein. Ein Testlauf mit den übrigen Zutaten, aber ohne das Lernen, schnitt schlechter ab als das lernende Programm.

Häufige Missverständnisse

• „Ein Gedächtnis hilft jeder Suche.“ Nein. Bei kleinen Aufgaben und bei der Taubenaufgabe bis sieben Löcher zeigte das Gedächtnis in der Messung keinen Vorteil.
• „Die neue Regel bringt dem Programm neues Wissen.“ Nein. Sie folgt aus den alten Regeln, ein unabhängiger Prüfer bestätigt das in den Tests der Demo. Sie erspart nur, dieselbe Folgerung noch einmal zu ziehen.

Wie ernst ist das Rechenbild zu nehmen?

Die Einladungsliste ist erfunden und bewusst klein. Gemessen wurde an zufälligen Aufgaben bis 110 Entscheidungen, an Aufträgen und Rampen und an der Taubenaufgabe, mit einem einzigen einfachen Vergleichsprogramm. Über Aufgaben aus der Praxis und über andere Programme sagt diese Seite nichts.

Was Sie mitnehmen

• Scheitert eine Planung wiederholt an derselben Stelle, fragen Sie, welche Festlegungen daran beteiligt sind, und halten Sie diese als Regel fest.
• Fragen Sie bei jedem Vergleich, was gezählt wurde: Fehlschläge oder Sekunden.

Für Ihre Alltagsplanung bedeutet das: Eine kleine Planung, die nach wenigen Anläufen aufgeht, braucht diese Buchführung nach der Messung dieser Seite nicht; bei einer großen, in der Sie wiederholt an derselben Stelle scheitern, kann sie sich lohnen. Das ist eine Deutung der Messung, kein Messwert.

In der Demo sehen Sie eine kleine Formel Schritt für Schritt. Zum Verstehen brauchen Sie sie nicht. Der Knopf „Demo ausprobieren“ öffnet sie, der Knopf „Weiter zum Fachteil“ führt zum zweiten Teil.

Hinweis: Alle Demos rechnen mit synthetischen oder frei verfügbaren Beispieldaten und laufen auf einem externen Anbieter (Datenschutz). Bitte geben Sie darin keine vertraulichen oder personenbezogenen Daten ein. Die Ergebnisse gelten für die jeweilige Demo-Instanz und lassen sich nicht ungeprüft auf reale Fälle übertragen; für darauf gestützte Entscheidungen übernehme ich keine Gewähr.

Modell und Annahmen

Dieser Teil ist eigenständig lesbar. Es geht um den Vergleich eines Lösers mit Konfliktlernen (CDCL, conflict-driven clause learning) und einer Suche ohne Gedächtnis (DPLL) auf Erfüllbarkeitsaufgaben. Das Maß ist die Zahl der Fehlschläge, nicht die Zeit.

• Formel: Eine Formel in konjunktiver Normalform \(F = C_1 \wedge \dots \wedge C_m\) über den Variablen \(x_1, \dots, x_n\). Jede Klausel \(C_j\) ist eine Oder-Verknüpfung von Literalen \(x_i\) oder \(\neg x_i\). Gesucht ist eine erfüllende Belegung oder der Nachweis, dass es keine gibt. Literale sind im Programm ganze Zahlen (−5 steht für „nicht \(x_5\)“). Formelerzeuger und Zufallsgenerator (SplitMix64, ganzzahlig, auf jeder Plattform derselbe Strom) stammen aus einem gemeinsamen Kern-Paket der Reihe; Python-random und hash() kommen nirgends vor.
• Konfliktlernen (CDCL): Der Löser belegt eine Variable (eine Entscheidung, eine neue Stufe) und erzwingt daraus, was die Klauseln zwingend verlangen (Einheitspropagation). Wird eine Klausel falsch, ist das ein Konflikt. Rückwärts entlang der Belegungsreihenfolge wird aufgelöst, bis auf der Konfliktstufe genau ein Literal übrig ist (1-UIP, erste eindeutige Implikationsstelle). Das Ergebnis ist die gelernte Klausel; der Löser springt auf die zweithöchste Stufe in ihr zurück. Standardlöser der Messreihen: Aktivität je Variable (VSIDS in der MiniSat-Variante), Phasenspeicher, Luby-Neustarts mit Einheit 32, ohne Minimieren, mit zwei beobachteten Literalen.
• Suche ohne Gedächtnis (DPLL): Einheitspropagation und die Regel „häufigste Variable, erst wahr“. Bei einem Widerspruch kehrt die Suche nur eine Stufe zurück. In Experiment 1 der Demo gilt für beide Löser die feste Reihenfolge \(x_1, x_2, \dots\) mit „wahr zuerst“, damit sich jeder Schritt von Hand nachrechnen lässt.
• Aufwand: Gezählt werden CDCL-Konflikte und DPLL-Widersprüche, nie Sekunden. Ein Widerspruch ist ein Blatt der DPLL-Suche, an dem die Einheitspropagation eine leere Klausel erzeugt; er entspricht einem CDCL-Konflikt. Die Sackgassen des DPLL (Blätter und innere Knoten, deren beide Zweige scheitern) stehen nur als Nebenzahl da. Wer CDCL-Konflikte gegen DPLL-Sackgassen stellt, überzeichnet den Vorsprung bei unerfüllbaren Formeln etwa um den Faktor 2; die Demo tut das nicht.
• Messzellen: Je Zelle feste Formeln, CDCL-Konflikte gegen DPLL-Widersprüche, vorgerechnet und nicht live (39 Zellen in einer Datei, die die App liest). Der Quotient ist der Median der DPLL-Widersprüche durch den Median der CDCL-Konflikte (Verhältnis der Mediane, nicht Median der Verhältnisse). Unter 1,2 lautet das Verdikt der Demo „kein Vorsprung“; die Schwelle ist eine Festlegung der Demo.
• Instanzfamilien: Zufalls-3-SAT mit \(n = 30\) bis 110 Variablen und Klauseln je Variable \(m/n = 4,0\), 4,26 und 4,5; Aufträge auf Rampen (Färbung eines Konfliktgraphen mit 3 Rampen); Schur-Zahlen mit 3 Mengen; Schubfach mit \(h + 1\) Tauben und \(h\) Löchern (unerfüllbar).

Die Formeln

Auflösung (Resolution). Aus zwei Klauseln mit gegensätzlichem Literal folgt die Resolvente:

\[(A \vee x) \wedge (B \vee \neg x) \;\Longrightarrow\; (A \vee B).\]

Gelernte Klausel (1-UIP). \(\mathrm{lvl}(\ell)\) ist die Entscheidungsstufe, auf der das Literal \(\ell\) wahr wurde, \(d\) die Konfliktstufe und \(C_k\) die verletzte Klausel. Ausgehend von \(C_k\) wird in umgekehrter Reihenfolge der Belegung jeweils das letzte Literal der Stufe \(d\) mit seiner Begründung aufgelöst, bis genau ein Literal \(u\) der Stufe \(d\) übrig bleibt (die erste eindeutige Implikationsstelle):

\[L = C_k \;\overset{\text{Auflösungen}}{\longrightarrow}\; \bigl(\neg u \vee R\bigr), \qquad \mathrm{lvl}(r) < d \text{ für alle } r \in R.\]

Rücksprungstufe. Die gelernte Klausel wird nach dem Rücksprung sofort zur Einheit:

\[\beta = \max\{\mathrm{lvl}(r) : r \in R\} \quad (\beta = 0 \text{ bei } R = \emptyset).\]

Die Stufen \(\beta + 1, \dots, d - 1\) werden übersprungen.

Folgerichtigkeit. Jede gelernte Klausel \(L\) folgt aus den Klauseln davor durch Einheitspropagation unter der Verneinung von \(L\) (RUP, reverse unit propagation). Der Test der Demo prüft das mit einem unabhängigen Prüfer.

Zählweise der Suche ohne Gedächtnis. Im Suchbaum des DPLL hat jeder Knoten null Kinder (ein Blatt mit Widerspruch) oder zwei. \(W\) ist die Zahl der Widersprüche, \(S\) die der Sackgassen, \(N\) die der Knoten. Ist die Formel unerfüllbar, sind alle Blätter Widersprüche, und der Baum hat

\[N = 2W - 1 \quad \text{Knoten, und alle sind Sackgassen: } S = N.\]

Der Vergleich mit dem CDCL nimmt deshalb \(W\) (der Widerspruch ist das Gegenstück zum Konflikt) und nicht \(S\).

Herleitung Schritt für Schritt

Die Schritte rechnen das erfundene Beispiel aus Teil 1 mit den Formeln oben durch. Sie sind Rechnung dieser Seite, keine Messung der Demo.

• Schritt 1, Klauseln: Anna \(= x_1\), Gustav \(= x_2\), Hanna \(= x_3\), Dora \(= x_4\), Erwin \(= x_5\), Frieda \(= x_6\). Die drei Regeln sind \((\neg x_4 \vee x_5)\), \((\neg x_4 \vee x_6)\) und \((\neg x_1 \vee \neg x_5 \vee \neg x_6)\).
• Schritt 2, Entscheidungen und Konflikt: Die Entscheidungen \(x_1\), \(x_2\), \(x_3\), \(x_4\) liegen auf den Stufen 1 bis 4, jeweils mit „wahr“. Auf Stufe 4 erzwingt die Einheitspropagation \(x_5\) (Begründung \(\neg x_4 \vee x_5\)) und \(x_6\) (Begründung \(\neg x_4 \vee x_6\)). Damit ist die dritte Klausel falsch: Konflikt auf der Konfliktstufe \(d = 4\), \(C_k = (\neg x_1 \vee \neg x_5 \vee \neg x_6)\).
• Schritt 3, Analyse: \(C_k\) enthält zwei Literale der Stufe 4. Das später belegte, \(x_6\), wird mit seiner Begründung aufgelöst: Es entsteht \((\neg x_1 \vee \neg x_4 \vee \neg x_5)\). Dann wird \(x_5\) aufgelöst: Es entsteht \((\neg x_1 \vee \neg x_4)\). Auf Stufe 4 bleibt nur \(\neg x_4\) übrig, also \(u = x_4\) und \(R = \{\neg x_1\}\). Gelernt ist \((\neg x_1 \vee \neg x_4)\): Anna und Dora nicht beide.
• Schritt 4, Rücksprung: \(\beta = \mathrm{lvl}(x_1) = 1\). Die Stufen 2 und 3 (Gustav, Hanna) werden übersprungen. Nach dem Rücksprung ist die gelernte Klausel eine Einheit und erzwingt \(x_4 = \text{falsch}\) schon auf Stufe 1.
• Schritt 5, Folgerichtigkeit: Setzt man \(x_1\) und \(x_4\) auf „wahr“, erzwingt die Einheitspropagation \(x_5\) und \(x_6\) und verletzt die dritte Klausel. Also folgt \((\neg x_1 \vee \neg x_4)\) aus den drei Klauseln durch Einheitspropagation unter der Verneinung (RUP).
• Schritt 6, Zählweise: Ein Baum, in dem jeder innere Knoten genau zwei Kinder und jedes Blatt keines hat, hat einen inneren Knoten weniger als Blätter. Bei \(W\) Blättern sind das \(W - 1\) innere Knoten und \(N = 2W - 1\) Knoten insgesamt. Bei einer unerfüllbaren Formel scheitern alle Zweige, also ist jeder Knoten eine Sackgasse.

Durchgerechnet: das Handbeispiel der Demo

Das Handbeispiel F1 der Demo hat fünf Klauseln über \(x_1\) bis \(x_6\), die feste Reihenfolge \(x_1, x_2, \dots\) und „wahr zuerst“. Die DPLL-Suche braucht 14 Knoten mit 6 Widersprüchen und 11 Sackgassen; Schritt 6 bestätigt \(2 \cdot 6 - 1 = 11\) (Rechnung dieser Seite). Der CDCL hat 2 Konflikte:

• Konflikt 1 auf Stufe 5 in K2: gelernt \((\neg x_1 \vee \neg x_5)\), Sprung auf Stufe 1, die Stufen 2, 3 und 4 werden übersprungen. Nach der Formel oben ist \(u = x_5\) auf der Konfliktstufe 5 und \(R = \{\neg x_1\}\), also \(\beta = \mathrm{lvl}(x_1) = 1\) (Rechnung dieser Seite).
• Konflikt 2 auf Stufe 1 in K4: gelernt \((\neg x_1)\), Sprung auf Stufe 0. Hier ist \(R = \emptyset\), also \(\beta = 0\) (Rechnung dieser Seite).

Das Beispiel ist von Hand nachgerechnet und im Test gegen einen unabhängigen DPLL-Zähler geprüft. Beim Schubfach mit \(h = 2\) (3 Tauben, 2 Löcher) braucht der DPLL 3 Knoten mit 2 Widersprüchen; auch das passt zu \(N = 2W - 1\). Ein Einzelfall sagt nichts über die Messreihen.

Befunde

Alle Zahlen sind Messungen der Demo und gelten nur für die genannte Voraussetzung. Messzellen: je 20 feste Formeln (Zufalls-Seeds 1 bis 20), Schur und Schubfach je eine Formel; Experiment 4 (gelernte Klauseln) je 12 feste Formeln. Aufwand in Konflikten und Widersprüchen. Kein Lauf brach am Budget ab (CDCL-Budget 200.000 Konflikte, DPLL-Budget 50.000 Knoten, beim Schubfach 200.000).

Wächst der Vorsprung mit \(n\)? Zufalls-3-SAT, \(m/n = 4,26\), 20 Formeln. Median der CDCL-Konflikte, Median der DPLL-Widersprüche, Quotient (DPLL-Widersprüche durch CDCL-Konflikte), Zahl erfüllbarer Formeln von 20 und Median der DPLL-Sackgassen:

\(n\)	CDCL-Konflikte	DPLL-Widersprüche	Quotient	erfüllbar	DPLL-Sackgassen
30	14,5	6,5	0,45	12	10
50	35	39,5	1,13	13	75,5
70	89	104	1,17	11	205
90	159	343,5	2,16	13	680
110	287	1.014,5	3,53	13	2.024,5

Der Quotient wächst in allen vier Schritten; unter 1,2 (Verdikt „kein Vorsprung“) liegt er bei \(n = 30\) bis 70.

Wie fest ist diese Grenze? Quotient bei \(m/n = 4,26\) mit drei Formelmengen (Zufalls-Seeds 1 bis 20, 21 bis 40 und 41 bis 60):

\(n\)	Seeds 1 bis 20	Seeds 21 bis 40	Seeds 41 bis 60
30	0,45	0,88	0,84
50	1,13	0,81	1,18
70	1,17	1,45	0,90

Bei \(n = 90\) lag der Quotient in einer Nachprüfung mit denselben beiden anderen Formelmengen bei 2,34 und 1,71 (nicht Teil der Tests). „Ab etwa \(n = 90\) zahlt sich das Lernen aus“ gilt also für diese Instanzfamilie und ist unscharf: Zwischen \(n = 50\) und 70 streut der Quotient um mehrere Zehntel.

Hängt das am Verhältnis \(m/n\)? Ja. Quotient für \(n = 30, 50, 70, 90, 110\), je 20 Formeln:

\(m/n\)	30	50	70	90	110
4,0	0,24	0,97	0,80	1,52	0,84
4,26	0,45	1,13	1,17	2,16	3,53
4,5	0,68	1,05	1,24	1,42	2,17

Bei \(m/n = 4,5\) wächst der Quotient ebenfalls in allen vier Schritten; erfüllbar sind dort 11 / 9 / 5 / 5 / 5 von 20 Formeln. Bei \(m/n = 4,0\) wächst er nicht: Dort sind bei \(n = 90\) 19 von 20 und bei \(n = 110\) alle 20 Formeln erfüllbar, und das Lernen hat gegenüber dem DPLL bei \(n = 110\) keinen Vorsprung.

Aufträge auf Rampen. Färbung des Konfliktgraphen mit 3 Rampen, 20 Formeln je Zelle, nach mittlerem Grad. Quotient bei \(n = 30\) / 60 / 90 und Zahl erfüllbarer Formeln von 20:

mittlerer Grad	Quotient	erfüllbar
4,0	1,83 / 0,86 / 0,86	14 / 19 / 18
4,5	1,00 / 1,62 / 1,8	2 / 7 / 9
5,0	1,11 / 1,23 / 1,5	1 / 0 / 0

Bei Grad 4,5 sind es CDCL 15 / 19,5 / 29,5 Konflikte gegen DPLL 15 / 31,5 / 53 Widersprüche. Bei Grad 4,0 (meist erfüllbar) liegt der Quotient für \(n = 60\) und 90 unter 1.

Schur-Zahlen und Schubfach. Schur mit 3 Mengen: \(n = 14\) (unerfüllbar) CDCL 148 Konflikte gegen DPLL 147 Widersprüche (Quotient 0,99; 293 Sackgassen); \(n = 13\) (erfüllbar) 18 gegen 10. Schubfach (\(h + 1\) Tauben, \(h\) Löcher, unerfüllbar), eine Formel je \(h\):

\(h\)	CDCL-Konflikte	DPLL-Widersprüche	Quotient
3	7	6	0,86
4	28	24	0,86
5	159	120	0,75
6	1.004	720	0,72
7	4.811	5.040	1,05
8	27.932	40.320	1,44

Gegenüber diesem DPLL hat der CDCL beim Schubfach bis \(h = 7\) keinen Vorsprung in der Zählung (Quotient unter 1,2); bei \(h = 8\) liegt der DPLL darüber. Die DPLL-Widersprüche sind in dieser Messung genau \(h!\). Von Zelle zu Zelle wächst der CDCL-Median um das 4,0- bis 6,3-Fache, der DPLL-Median um das 4,0- bis 8,0-Fache; beide Zähler wachsen mit jedem Loch weiter.

Zählweise. In allen 228 unerfüllbaren Messzeilen (Zufall, Rampen, Schur, Schubfach) ist die Zahl der Sackgassen genau \(2W - 1\). Bei \(m/n = 4,26\) liegt der Median der Sackgassen je Widerspruch bei \(n = 50, 70, 90, 110\) bei 1,94 / 1,98 / 1,98 / 1,99.

Was wird gelernt? Zufalls-3-SAT, \(m/n = 4,26\), je 12 Formeln, Mediane, ohne gegen mit Minimieren der gelernten Klausel:

\(n\)	Konflikte	mittlere Länge	Formeln mit weniger / mehr Konflikten
50	22 gegen 22	5,1 gegen 4,4	3 / 3 (6 gleich viele)
150	3.370 gegen 2.845,5	11,9 gegen 9,5	7 / 5

Bei \(n = 150\) sind das 15,6 % weniger Konflikte (Bezug: ohne Minimieren). Die Länge sinkt in beiden Größen; die Konfliktzahl nur bei \(n = 150\) im Median, aber bei 5 von 12 Formeln steigt sie dort: Mit 12 Formeln ist das keine gesicherte Wirkung. Die mittlere Sprungweite (Konfliktstufe minus Rücksprungstufe) liegt bei 1,2; nur 14,8 % der Sprünge (\(n = 50\), ohne Minimieren; mit Minimieren 12,2 %) beziehungsweise 13,3 % (\(n = 150\); 12,8 %) gehen über mehr als eine Stufe. Das Überspringen mehrerer Stufen ist in diesen Läufen die Ausnahme.

Grenzen: was die Messung zeigt und was nicht

• Ein DPLL, nicht „die Suche ohne Gedächtnis“: Verglichen wird mit der Rekursion mit Listenkopie, Einheitspropagation und der Regel „häufigste Variable“. Mit einer anderen Verzweigungsregel ändern sich die Widerspruchszahlen; das Verhältnis gilt für dieses Paar.
• Der Quotient misst nicht das Lernen allein: Er vermischt das Lernen mit Verzweigungsregel, Phasenspeicher und Neustarts. In einer Nachprüfung (nicht Teil der Tests) braucht ein Löser mit denselben Aktivitäten ohne Lernen bei Zufalls-3-SAT (\(m/n = 4,26\)) und \(n = 90\) im Median 6.611,5 Konflikte statt 159, am Schubfach 52 / 375 / 3.246 statt 28 / 159 / 1.004 bei \(h = 4, 5, 6\).
• Instanzfamilien und Größen: Zufalls-3-SAT bis \(n = 110\) (je 20 Formeln; in den Zellen eine Formelmenge), Rampen bis \(n = 90\), Schur nur mit 3 Mengen, Schubfach bis \(h = 8\). Aussagen über größere \(n\), Industrieformeln oder andere Löser (Kissat, CaDiCaL) macht die Demo nicht. „Wächst mit \(n\)“ gilt nur für die gemessenen \(n\).
• Konflikte sind keine Zeit: Ein CDCL-Konflikt (Analyse, Lernen) kostet mehr Arbeit als ein DPLL-Widerspruch. Die Zeit je Konflikt ist nicht gemessen; die Demo macht keine Aussage über Laufzeiten.
• Medianvergleiche mit 20 Formeln: Der Quotient ist ein Verhältnis der Mediane. Die Schwelle 1,2 ist eine Festlegung der Demo. Bei \(n = 50\) bis 70 streut der Quotient mit der Formelmenge um mehrere Zehntel (siehe Befunde).
• Ursachen sind Deutungen: Warum der Vorsprung bei \(m/n = 4,0\) ausbleibt oder die DPLL-Widersprüche beim Schubfach \(h!\) betragen, ist nicht untersucht; die Demo zeigt nur die Messung.
• Schritt-für-Schritt-Ansicht: nur für kleine Formeln (höchstens 12 Variablen und 60 Klauseln). Sie zeigt den Lauf mit fester Reihenfolge, nicht den Standardlöser der Messreihen.
• Quellenlage: GRASP ist für Konfliktklauseln aus dem Implikationsgraphen und das nichtchronologische Zurückspringen gelesen. Die Wahl des First UIP nennt das Glucose-Papier; ob GRASP selbst den ersten UIP als Standard nimmt, wurde nicht geprüft.

Erweiterungen und Verweise

Nicht umgesetzt sind eigene Verzweigungsregeln, Neustarts, das Löschen gelernter Klauseln und die Datenstrukturen des Lösers (sie sind Gegenstand der Folgestücke der Reihe), ein Beweisprotokoll mit Prüfer als Demo-Inhalt, Zeitmessungen, lateinische Quadrate als Instanzfamilie und die Live-Rechnung der großen Zellen. Verweise (Angaben nach der README der jeweiligen Demo):

• DPLL und Phasenübergang: Die SAT-Demo zum Phasenübergang zeigt die Suche ohne Gedächtnis und baut das Klausellernen ausdrücklich nicht; dazu gibt es die Erklärseite zum Phasenübergang bei SAT.
• Gleiches Kernmodell, andere Frage: Die Demo zur Graphfärbung hat dasselbe Kernmodell wie die Rampen-Aufgabe, fragt aber nach der Reihenfolge des Färbens.

Quellen

• Marques-Silva, J. P., & Sakallah, K. A. (1999): GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5), 506–521.
• Audemard, G., & Simon, L. (2009): Predicting learnt clauses quality in modern SAT solvers. IJCAI 2009.
• Haken, A. (1985): The intractability of resolution. Theoretical Computer Science 39, 297–308; nach Beame, P., Pitassi, T., & Impagliazzo, R. (1993): Exponential lower bounds for the pigeonhole principle. Computational Complexity 3, 97–140.

Die Angaben stammen aus der Quellenliste der Demo, dort anhand der Quellen geprüft: von Marques-Silva und Sakallah sind die Einleitung und die Abschnitte 2 und 3.1 gelesen, von Audemard und Simon die Abschnitte 3, 4 und 6. Haken ist nur im Abstract gelesen; die Aussage, dass Resolutionsbeweise des Schubfachprinzips exponentiell lang sind, steht nach Beame, Pitassi und Impagliazzo (Einleitung gelesen). Gelernte Klauseln sind Resolventen; die Folgerung für den CDCL ist eine eigene, in den gelesenen Quellen nicht ausdrücklich genannte.