Symmetrie brechen bei SAT verständlich erklärt

Neun Lastwagen sollen entladen werden, aber es gibt nur acht Rampen, und alle Rampen sind gleich. Ein Programm, das prüft, ob sich alle Bedingungen eines Plans zugleich erfüllen lassen (Fachwort: SAT), kann jede Vertauschung der Rampen noch einmal durchprobieren. „Symmetrie brechen“ heißt, das zu verhindern: Von vertauschbaren Dingen wird nur eine Anordnung probiert. In der Messung sinkt die Zahl der Sackgassen (Fehlversuche des Programms) dadurch bei acht Rampen von 27.932 auf 1. Die Seite zeigt, was das bringt und wo der Nutzen nicht belegt ist.

Zuletzt aktualisiert: 11. November 2026

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

Neun Lastwagen, acht gleiche Rampen

Stellen Sie sich einen Hof mit acht Laderampen vor. Alle Rampen sind gleich: gleich breit, gleich nah am Lager. Neun Lastwagen wollen entladen, und jeder braucht eine eigene Rampe.

Sie sehen sofort, dass das nicht aufgeht: Es sind mehr Lastwagen als Rampen. Ein Rechenprogramm, das solche Aufgaben löst, zählt nicht so geschickt. Es probiert: der erste Lastwagen an die erste Rampe, der zweite an die zweite, und so weiter, bis für den neunten keine Rampe mehr frei ist. Das ist eine Sackgasse. Dann geht das Programm einen Schritt zurück und probiert für den zuletzt festgelegten Lastwagen eine andere Rampe.

Hier liegt das Problem. Weil alle Rampen gleich sind, ist es für die Aufgabe egal, ob der erste Lastwagen an die erste oder an die dritte Rampe fährt. Eine Sackgasse, die bei einer Verteilung auftritt, tritt bei jeder Verteilung mit vertauschten Rampen genauso auf. Das Programm merkt das nicht und sucht sie jedes Mal neu. Fachleute nennen vertauschbare Dinge symmetrisch.

Beispiel: Bei drei gleichen Rampen gibt es sechs Arten, sie umzunummerieren (drei mal zwei mal eins). Nutzt eine Verteilung alle drei Rampen, erscheint sie also in sechs Fassungen, und jede Sackgasse auch.

Die Regel: Rampen der Reihe nach benutzen

Abhilfe schafft eine zusätzliche Regel. Sie verbietet nur, eine Rampe anzufahren, die in der Reihenfolge zu weit hinten liegt: Die zweite Rampe darf erst benutzt werden, wenn ein früherer Lastwagen die erste benutzt, die dritte erst, wenn die zweite benutzt wird, und so weiter. Von allen umnummerierten Fassungen einer Verteilung bleibt eine erlaubt: die, in der die Rampen von vorn nach hinten gefüllt werden.

Die Antwort der Aufgabe ändert die Regel nicht. Gibt es eine Verteilung, bleibt auch mit der Regel eine übrig, man nummeriert die Rampen einfach um. Gibt es keine, gibt es auch mit der Regel keine. Nur die Zahl der Verteilungen schrumpft: Bei zwei Lastwagen und zwei Rampen gibt es zwei Verteilungen, mit der Regel eine. Wer alle Verteilungen aufzählen will, kann die Regel deshalb nicht verwenden.

Was das beim Entladen ausmacht

Mit der Regel muss der erste Lastwagen an die erste Rampe, der zweite an die zweite, und so fort. Diese Folgen ergeben sich zwingend: Das Programm muss dafür keine Möglichkeiten durchprobieren. Beim neunten Lastwagen steht der Widerspruch deshalb sofort fest.

Ein Lauf ist ein Versuch des Programms, die Aufgabe zu lösen. In der Messung zu dieser Seite brauchte es bei acht Rampen und neun Lastwagen ohne die Regel 27.932 Sackgassen, mit der Regel 1, je in einem Lauf. Mit jeder zusätzlichen Rampe stieg die Zahl der Sackgassen ohne Regel auf mindestens das Vierfache der vorigen Zahl, mit der Regel blieb sie bei 1. Gezählt wurden Sackgassen, keine Sekunden.

Zweites Bild: Zahlenkarten auf Körbe verteilen

Dieselbe Idee wirkt auch ohne Lastwagen. Sie haben Karten mit den Zahlen von 1 bis 44 und vier Körbe. Jede Karte kommt in genau einen Korb. In keinem Korb dürfen zwei Karten liegen, deren Summe als dritte Karte im selben Korb liegt (auch zwei gleiche Karten zusammen gelten). Mit den Karten zwei, drei und fünf: Liegen die zwei und die drei im selben Korb, darf die fünf nicht dazu. Bis zu 44 Karten gibt es eine solche Verteilung.

Auch hier sind die Körbe vertauschbar. Die Regel lautet: Der zweite Korb wird erst benutzt, wenn schon eine frühere Karte im ersten liegt, der dritte erst nach dem zweiten, und so weiter. Bei 44 Karten brauchte das Programm ohne die Regel 108.775 Sackgassen, mit der Regel 3.844, wieder je ein Lauf.

Dieselbe Regel passt auf Aufträge, von denen manche nicht an dieselbe Rampe dürfen, etwa weil zwei Lieferanten sich nicht begegnen sollen. Welche Rampe jeder bekommt, ist egal, solange solche Aufträge getrennt bleiben. Die Regel lautet dort: Die Aufträge der ersten zwei Lieferanten, die sich nicht begegnen dürfen, bekommen die ersten beiden Rampen.

Wo die Regel nicht sicher hilft

Die Regel ist kein Zaubermittel. Bei einer leichteren Aufgabe mit 43 Karten brauchte der erste Lauf ohne Regel nur 6 Sackgassen, mit Regel 352. Vermutlich liegt das daran, dass die Regel einschränkt, in welcher Reihenfolge das Programm seine Entscheidungen sucht; die Ursache wurde nicht untersucht.

Ein einzelner Lauf ist aber ein Einzelfall. Der erste Lauf kommt ohne Zufall aus. Für weitere Läufe würfelt das Programm vorab eine zufällige Vorliebe aus, welche Entscheidung es zuerst probiert; die Zahl, die diesen Zufall festlegt, heißt Zufalls-Seed. Bei 20 solchen Läufen brachte die Regel in der Hälfte mehr Sackgassen und in der anderen Hälfte weniger. Der Unterschied ist damit nicht belegt, das heißt: nicht größer als der Zufall zwischen den Läufen. Eine Kontrolle mit weiteren Läufen kehrte die Richtung um, über alle Läufe zusammen ist wieder nichts belegt. Aus einem oder zwanzig Läufen lässt sich die Richtung also nicht ablesen.

Über alle zehn gemessenen Aufgabengrößen (vier mit Zahlenkarten, sechs mit Aufträgen, die nicht an dieselbe Rampe dürfen) ergab sich:

• in sechs Größen half die Regel belegt,
• in keiner schadete sie belegt,
• in einer war es etwa gleich,
• in drei war kein Unterschied belegt.

Häufige Missverständnisse

• „Mit der Regel ändert sich die Antwort.“ Nein. Ob es eine Lösung gibt, bleibt gleich. Nur der Weg dorthin wird kürzer, in einzelnen Läufen auch länger.
• „Weniger Sackgassen heißt weniger Rechenzeit.“ Das ist nicht gemessen. Die Regel fügt Bedingungen hinzu, und Sackgassen sind nicht gleich teuer.
• „Gleiche Dinge auseinanderzuhalten lohnt immer.“ Nein. Bei den Lastwagen und Rampen war der Gewinn groß, bei leichten Zahlenaufgaben ist ein Nutzen nicht belegt.

Woran Sie das im Alltag erkennen

• Ihre Planung enthält mehrere gleiche Plätze, Maschinen oder Schichten. Dann kann sich dieselbe Sackgasse in jeder Vertauschung wiederholen.
• Ein Planungsprogramm braucht lange, um zu melden, dass etwas nicht geht, obwohl Sie das durch Zählen sofort sehen.

Wie ernst ist das Rechenbild zu nehmen?

Gemessen wurde mit einem einzigen Rechenprogramm und drei Aufgabenarten: Lastwagen auf Rampen, Zahlenkarten auf Körbe, unverträgliche Aufträge auf Rampen. Andere Programme, andere Einstellungen und Aufgaben aus der Praxis wurden nicht gemessen.

Was Sie mitnehmen

• Fragen Sie bei gleichen Plätzen, Maschinen oder Farben, ob ein Programm jede Vertauschung einzeln durchprobiert.
• Eine Regel „der Reihe nach“ ändert nicht die Antwort, nur den Weg dorthin.
• Prüfen Sie einen Gewinn oder Schaden an mehreren Läufen, nicht an einem einzelnen.

Zu dieser Seite gehört ein Programm zum Ausprobieren im Browser, die Demo. Dort stellen Sie Aufgaben ein und sehen die Sackgassen mit und ohne Regel. Zum Verstehen brauchen Sie sie nicht. Der Knopf „Demo ausprobieren“ öffnet sie, der Knopf „Weiter zum zweiten Teil“ führt zum zweiten Teil für Fachleute.

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. Er behandelt Symmetriebrechung für SAT-Löser mit Konfliktlernen (CDCL): zusätzliche Klauseln, die von jeder Bahn einer Symmetrie nur einen Vertreter zulassen, und die Frage, was das an der Zahl der Konflikte ändert.

• Aufgabe: Gegeben ist eine Formel \(F\) in konjunktiver Normalform und eine Gruppe \(G\) von Umbenennungen der Variablen, die jede Lösung von \(F\) in eine Lösung von \(F\) überführen (eine Symmetrie). Gesucht ist \(F' = F \wedge R\), das genauso erfüllbar ist wie \(F\) und von jeder Bahn der Gruppe nur einen Vertreter zulässt; \(R\) ist eine Liste zusätzlicher Klauseln. Es gibt drei von Hand geschriebene Regeln, keine allgemeine Symmetrieerkennung.
• Aufgabenfamilien: Schubfach: \(h + 1\) Aufträge, \(h\) Rampen, jeder Auftrag mindestens eine Rampe, jede Rampe höchstens einen Auftrag; unerfüllbar. Mit genau \(h\) Aufträgen ist die Aufgabe erfüllbar und hat \(h!\) Lösungen. Schur: die Zahlen 1 bis \(n\) auf \(k\) Mengen, in keiner Menge \(a + b = c\) (\(a = b\) erlaubt), jede Zahl in genau einer Menge; für \(k = 3\) ist die Aufgabe bis \(n = 13\) erfüllbar (durch Aufzählung bestätigt, \(S(3) = 13\)), für \(k = 4\) bis \(n = 44\) (nach Golomb und Baumert 1965 als zitierter Wert, die Quelle wurde nicht gelesen). Färbung: \(n\) Aufträge, Konfliktgraph mit mittlerem Grad 5 (SplitMix64), 3 Rampen; „höchstens eine Rampe“ fehlt bewusst, eine zweite Rampe schadet nicht.
• Löser: CDCL mit 1-UIP-Lernen, Aktivität je Variable (VSIDS in der MiniSat-Variante, Zerfall 0,95), Phasenspeicher, Luby-Neustarts (Einheit 32), Watched Literals, ohne Löschen. Der Standardlauf hat den Löser-Zufalls-Seed 0 ohne zufälligen Start der Aktivitäten. Die Löser-Zufalls-Seeds 1 und höher starten die Aktivitäten zufällig (SplitMix64); ohne diesen Start wirkt der Seed nicht, alle Seeds wären derselbe Lauf.
• Messgröße: Konflikte (Widersprüche, auf die der Löser beim Propagieren stößt) bis zur Antwort; ein Abbruch am Budget zählt mit dem Budget (untere Schranke). Budgets: Schubfach 100.000, Schur mit 4 Mengen 300.000, Färbung 100.000 Konflikte. Sekunden werden nicht gemessen.
• Einordnung (Schwellen vor der Messung festgelegt): Quotient der Konflikte mit und ohne Regel unter 0,8 „weniger“, über 1,2 „mehr“, sonst „etwa gleich“; sind beide Zahlen höchstens 10, gilt „etwa gleich“. Über viele Läufe gelten „weniger“ und „mehr“ nur bei einem Test mit \(p < 0,05\) (Rangsummentest nach Mann-Whitney für die Löser-Zufalls-Seeds, exakter Vorzeichentest für die Graphen der Färbung, weil jeder Graph ohne und mit Regel gerechnet wird), sonst „nicht belegt“. Der Test kam nach der ersten Messung hinzu, weil die Mediane der 20 Seeds die Aussage sonst scheinbar bestätigt hätten (Quotient 1,21).

Die Formeln

Die Regeln sind Listen von Klauseln über den Variablen \(x_{i,c}\) (Zahl oder Knoten \(i\) hat Farbe \(c\)) und \(x_{p,l}\) (Auftrag \(p\) fährt Rampe \(l\) an). Schur: Jede Zahl hat genau eine Farbe, und für \(a + b = c\) (auch mit \(a = b\)) liegen nie alle drei in derselben Farbe:

\[\neg x_{a,c} \vee \neg x_{b,c} \vee \neg x_{a+b,c} \qquad \text{für alle } a \le b,\ a + b \le n,\ c = 0, \dots, k-1.\]

Schubfach: Jeder Auftrag hat mindestens eine Rampe, jede Rampe höchstens einen Auftrag:

\[\bigvee_{l=0}^{h-1} x_{p,l} \quad (p = 0, \dots, h), \qquad \neg x_{p,l} \vee \neg x_{q,l} \quad (p < q).\]

Wertevorrang (Schur und Färbung): Farbe \(c \ge 1\) darf nur vergeben werden, wenn eine frühere Zahl die Farbe \(c-1\) hat:

\[\neg x_{i,c} \vee \bigvee_{j < i} x_{j,c-1} \qquad \text{für } i \text{ in der Reihenfolge der Zahlen},\ c = 1, \dots, k-1.\]

Das sind \((k-1)\,n\) Klauseln; für die erste Zahl ist die Klausel die Einheitsklausel \(\neg x_{1,c}\). Lochvorrang (Schubfach): Auftrag \(p\) darf Rampe \(l \ge 1\) nur anfahren, wenn ein früherer Auftrag Rampe \(l-1\) anfährt:

\[\neg x_{p,l} \vee \bigvee_{q < p} x_{q,l-1} \qquad \text{für } p = 0, \dots, h,\ l = 1, \dots, h-1.\]

Das sind \((h-1)(h+1)\) Klauseln. Erste Kante fest (Färbung): für die erste Kante \(\{a, b\}\) des Graphen die Einheitsklauseln \(x_{a,0}\) und \(x_{b,1}\).

Herleitung Schritt für Schritt

Schritt 1, die Erfüllbarkeit bleibt erhalten (Beweisskizze der Demo). Sei \(\sigma\) eine Lösung von \(F\). Beim Wertevorrang nummeriert man die Farben nach ihrem ersten Auftreten um (nicht benutzte Farben zuletzt): Die neue Belegung ist eine Lösung von \(F\), weil eine Vertauschung der Farben eine Symmetrie ist, und sie erfüllt \(R\). Beim Lochvorrang ordnet man die besetzten Rampen nach dem kleinsten Auftrag darin; jede Rampe hat höchstens einen Auftrag, daher hat die Rampe \(l-1\) einen früheren Auftrag als die Rampe \(l\). Bei der ersten Kante sind \(a\) und \(b\) verschieden gefärbt, man macht ihre Farben zu 0 und 1. Umgekehrt ist jede Lösung von \(F \wedge R\) eine Lösung von \(F\), weil nur Klauseln hinzukommen. Also ist \(F\) genau dann erfüllbar, wenn \(F \wedge R\) erfüllbar ist.

Schritt 2, die Lösungen bleiben nicht erhalten. Benutzt eine Lösung \(m\) der \(k\) Farben, hat ihre Bahn unter den \(k!\) Farbvertauschungen \(k!/(k-m)!\) Elemente; für \(m \ge k-1\) sind das \(k!\). Benutzt jede Lösung mindestens \(k-1\) Farben, gilt

\[\#\text{Lösungen mit Wertevorrang} = \#\text{Bahnen} = \frac{\#\text{Lösungen}}{k!}.\]

„Lösungen geteilt durch \(k!\)“ ist nur dann die Zahl der Bahnen, wenn jede Lösung mindestens \(k-1\) Farben benutzt; bei \(n = 1\) und \(k = 3\) ist die Bahn nur 3 groß. Wer alle Lösungen braucht (zählen, Modelle aufzählen), kann die Regeln nicht verwenden; wer nur wissen will, ob eine Lösung existiert, kann es.

Schritt 3, warum der Lochvorrang das Schubfach schon durch Einheitspropagation erledigt (Rechnung dieser Seite; die Demo misst den Konflikt auf Stufe 0 für \(h = 3\) bis 8). Behauptung: Nach Einheitspropagation gilt für \(p = 0, \dots, h-1\), dass \(x_{p,p}\) wahr und \(x_{p,l}\) für \(l \ne p\) falsch ist. Für \(p = 0\): Die Klausel des Lochvorrangs ist für \(l \ge 1\) die Einheitsklausel \(\neg x_{0,l}\); in der Klausel „mindestens eine Rampe“ bleibt dann nur \(x_{0,0}\). Schritt \(p\): Die Rampen \(l < p\) sind von den Aufträgen \(l\) besetzt, also ist \(x_{p,l}\) für \(l < p\) falsch („höchstens ein Auftrag“). Für \(l > p\) sind alle \(x_{q,l-1}\) mit \(q < p\) falsch, denn Auftrag \(q\) hat nur Rampe \(q\) und \(q < p \le l-1\); die Klausel des Lochvorrangs erzwingt \(\neg x_{p,l}\). Es bleibt \(x_{p,p}\), das die Klausel „mindestens eine Rampe“ erzwingt. Für den letzten Auftrag \(p = h\) sind alle \(h\) Rampen belegt: Die Klausel „mindestens eine Rampe“ ist leer, es entsteht ein Widerspruch ohne eine einzige Entscheidung.

Durchgerechnet: das Handbeispiel Schubfach mit h = 2

Drei Aufträge, zwei Rampen: Die Formel hat 9 Klauseln; der Lochvorrang fügt 3 hinzu (\((h-1)(h+1) = 3\)). Einheitspropagation ohne die Regel belegt 0 von 6 Variablen und findet keinen Widerspruch. Mit der Regel sind alle 6 von 6 Variablen belegt, und der Widerspruch entsteht ohne Entscheidung. Der CDCL braucht ohne Regel 2 Konflikte (1 Entscheidung), mit Regel 1 Konflikt (0 Entscheidungen). Die erfüllbare Fassung mit 2 Aufträgen hat 2 Lösungen, mit Regel 1.

Ein zweites Beispiel von Hand: Schur mit \(k = 3\) und \(n = 13\) hat 18 Lösungen in 3 Bahnen der Größe \(3! = 6\) und 3 Lösungen mit Wertevorrang, genau eine je Bahn.

Befunde

Alle Zahlen stammen aus der vorgerechneten Messdatei der Demo (nicht live gerechnet) oder sind Zählungen des deterministischen Standardlaufs; sie gelten nur für den beschriebenen Löser und die drei Aufgabenfamilien. „Ein Lauf“ heißt: ein Standardlauf, keine Verteilung.

Schubfach. Ein Lauf je \(h\), Budget 100.000, kein Abbruch. Der Faktor je zusätzliche Rampe liegt ohne Regel zwischen 4,0 und 6,3. Mit dem Lochvorrang sind es für jedes \(h\) 1 Konflikt und 0 Entscheidungen. Der Quotient von \(h = 3\) (7 gegen 1) gilt als „etwa gleich“, weil beide Zahlen höchstens 10 sind; die Zählung nennt deshalb „weniger“ in 5 von 6 Aufgaben.

\(h\) (Rampen)	Konflikte ohne Regel	mit Lochvorrang
3	7	1
4	28	1
5	159	1
6	1.004	1
7	4.811	1
8	27.932	1

Schur mit 3 Mengen. Ein Lauf je \(n\), live gerechnet. Der Schritt von 1 auf 2 Konflikte gilt als „etwa gleich“, weil beide Zahlen höchstens 10 sind. Für \(n = 14\) ist die Aufgabe unerfüllbar.

\(n\)	Konflikte ohne Regel	mit Wertevorrang
11	1	2
12	1	2
13	18	11
14	148	21

Schur mit 4 Mengen, Standardlauf. Ein Lauf je \(n\); alle Aufgaben der Tabelle liegen im erfüllbaren Bereich \(n \le 44\). Bei \(n = 44\) ist der Faktor 28,3. Bei den leichten Aufgaben der Tabelle verschlechtert die Regel den einen Standardlauf, bei \(n = 44\) verbessert sie ihn.

\(n\)	Konflikte ohne Regel	mit Wertevorrang
38	0	65
40	6	184
42	6	352
43	6	352
44	108.775	3.844

Dieselben leichten Aufgaben mit 20 Löser-Zufalls-Seeds. Median über die 20 Läufe; „mehr“ zählt die Läufe, in denen die Regel mehr Konflikte braucht. Der Rangsummentest ergibt in keiner Zeile einen belegten Unterschied.

\(n\)	Median ohne Regel	Median mit Wertevorrang	mit Regel mehr Konflikte in	\(p\) (Rangsummentest)
38	131,5	95,5	5 von 20	0,26
40	323	363	10 von 20	0,74
42	278	366	12 von 20	0,48
43	302,5	366	10 von 20	0,20

Der Fall \(n = 43\) genauer. Der Quotient 366 / 302,5 = 1,21 (+21 %) liegt außerhalb des Bandes, ist aber nicht belegt. Der kleinste der 20 Läufe ohne Regel braucht 38 Konflikte, der Standardlauf nur 6: Er ist ein außergewöhnlich günstiger Lauf, kein typischer. Eine Kontrolle mit 100 weiteren Seeds (21 bis 120) kehrt das Vorzeichen um: Die Regel braucht in 36 Läufen mehr, in 63 weniger und in 1 gleich viele Konflikte; das Maximum liegt bei 3.509 gegen 4.181 Konflikten.

Läufe	Median ohne Regel	Median mit Wertevorrang	Änderung	\(p\)
20 Seeds	302,5	366	+21 %	0,20
100 weitere Seeds (21 bis 120)	391,5	287	−27 %	0,011
alle 120 Seeds	342	318	−7 %	0,071

Die Zahl aus 20 Läufen ist also nicht stabil: Sie wechselt in der Kontrolle das Vorzeichen, und über alle 120 Läufe ist kein Unterschied belegt. Der Test über die 100 weiteren Seeds allein ist belegt, der über alle 120 nicht.

Färbung. Je 10 Graphen mit mittlerem Grad 5 und 3 Rampen, alle 30 unerfüllbar, Median der Konflikte. „Weniger“ zählt die Graphen von 10, für die die Regel weniger Konflikte braucht; der Vorzeichentest vergleicht je Graph ohne und mit Regel. Die Antworten sind in allen Regeln gleich.

\(n\)	ohne Regel	erste Kante fest	Wertevorrang	weniger (erste Kante) / \(p\)	weniger (Wertevorrang) / \(p\)
60	21,5	7	9	9 von 10 / 0,004	10 von 10 / 0,002
90	49	30,5	32,5	10 von 10 / 0,002	9 von 10 / 0,021
120	73	28,5	35,5	10 von 10 / 0,002	9 von 10 / 0,021

Mehr Konflikte mit der Regel hatte bei der ersten Kante kein Graph, beim Wertevorrang keiner bei \(n = 60\) und je einer bei \(n = 90\) und 120. Zählung über alle zehn Zellen (die vier Schur-Zellen \(n = 38, 40, 42, 43\) und die sechs Färbungs-Zellen): belegt weniger in 6, belegt mehr in 0, etwa gleich in 1 (Schur \(n = 40\)), nicht belegt in 3 (Schur \(n = 38, 42, 43\)).

Prüfung der Antworten. Beim Bau wurden 430 Zufallsaufgaben gerechnet (Färbungen, Schur-Aufgaben, Schubfach-Aufgaben): Die Antwort des CDCL ohne und mit jeder passenden Regel stimmt in allen mit OR-Tools CP-SAT überein, 0 Abweichungen. Dieser Lauf ist eine Messung des Baus, nicht Teil der Testsuite.

Grenzen: was die Messung zeigt und was nicht

• Ein Löser, drei Familien: „Weniger“ und „mehr“ gelten für diesen CDCL (Aktivität, Phasenspeicher, Luby-Neustarts) und diese Aufgaben. Andere Löser und Einstellungen, Zufalls-3-SAT (hat typischerweise keine Farbsymmetrie, nicht gemessen) und industrielle Formeln sind nicht gemessen.
• Ein Standardlauf ist ein Lauf: Für \(n = 43\) zeigt der Standardlauf 6 gegen 352, der Median über Seeds sagt etwas anderes (302,5 gegen 366, nicht belegt). Bei den großen Unterschieden (Schubfach 27.932 gegen 1, Schur \(n = 44\): Faktor 28,3) ist ein Lauf aussagekräftiger als ein Quotient von 1,2, aber auch dort eine Zählung, keine Verteilung.
• 20 Seeds sind wenig: Der Median von \(n = 43\) liegt bei +21 %, die 100 Kontroll-Seeds bei −27 %. Die Rangsummentests sind eine Normalnäherung auf Läufen mit stark streuenden Konfliktzahlen (Maximum bis 5.306).
• Die Färbungszahlen hängen am Graphenerzeuger: Eine Vormessung mit anderen Graphen ergab bei \(n = 90\) einen Median von 62 gegen 16, der Bau mit SplitMix64-Graphen 49 gegen 30,5 (erste Kante fest).
• Erfüllbarkeit, nicht Lösungen: Die Regeln erhalten die Erfüllbarkeit, nicht die Menge der Lösungen.
• Schubfach, eigene Messung: Dass der Lochvorrang das Schubfach durch Einheitspropagation erledigt, ist hier gemessen (Konflikt auf Stufe 0, \(h = 3\) bis 8); die Herleitung oben ist eine Rechnung dieser Seite. Krishnamurthy 1985 und Aloul u. a. (Shatter) wurden nicht gelesen; diese Seite sagt nichts über deren Ergebnisse.
• Zählgrößen statt Sekunden: Mit der Regel kommen Klauseln hinzu, und Konflikte sind nicht gleich teuer. Dass der Aufwand in Konflikten sinkt, heißt nicht, dass die Laufzeit im gleichen Verhältnis sinkt.

Erweiterungen und Verweise

Nicht gebaut sind eine allgemeine Symmetrieerkennung (Graphautomorphismen, Shatter), dynamische Symmetriebrechung während der Suche, die allgemeine lexikographische Ordnung (Lex-Leader), Cube-and-Conquer und Beweise der Brechung (DRAT) sowie die Messung mehrerer Löser und Einstellungen (Neustarts, Phasenspeicher aus). Verweise (Angaben nach der Beschreibung der jeweiligen Demo):

• Zählbedingungen: Die Demo kardinalitaet-kodieren-demo schreibt „höchstens \(k\) von \(n\)“ als Klauseln; vertauschbare Rampen, Farben oder Löcher machen dort jede Lösung und jede Sackgasse mehrfach.
• Lernen ohne Brechung: In der Demo konfliktlernen-demo ist das Schubfach die Grenze des Lernens; hier ist die Brechung der Ausweg.
• Dieselbe Färbung, andere Frage: Die Demo graph-coloring-demo färbt Graphen, ohne nach der Symmetrie zu fragen.
• Schubfach und Störung: Die Demo sat-phasenuebergang-demo misst Schubfach-Formeln mit einer einfachen Suche und die Wirkung kleiner Störungen.

Quellen

• Heule, M. J. H.: Schur Number Five. arXiv 1711.08076, 2017 (Volltext gelesen: Die Vertauschung der 5 Farben wird durch eine lexikographische Ordnung der Farben gebrochen; der Wertevorrang der Demo ist dieselbe Familie; \(S(3) = 13\) und \(S(4) = 44\) werden dort nach Golomb und Baumert 1965 zitiert).
• Crawford, J. u. a. (1996): im Heule-Papier als Quelle der lexikographischen Ordnung der Farben genannt; nicht gelesen.
• Golomb, S. W., & Baumert, L. D. (1965): Quelle von \(S(3) = 13\) und \(S(4) = 44\); nicht gelesen.

Für das Schubfach mit Symmetriebrechung wurde keine Quelle gelesen: Die Aussage dieser Seite ist eine eigene Messung der Demo. Die Angaben zu Crawford u. a. und zu Golomb und Baumert stammen aus dem Heule-Papier und aus der README der Demo, nicht aus den Originalen.