Lokale Suche gegen Lernen verständlich erklärt

Ein Dienstplan bricht noch eine Regel? Dann stellen Sie ihn um und prüfen neu, so lange, bis alle Regeln aufgehen. Oder Sie bauen ihn Stück für Stück auf und notieren jede Sackgasse als neue Regel. Die Messung hinter dieser Seite zeigt, wann welcher Weg weniger Arbeit braucht und was nur einer von beiden kann. 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.

Ein Dienstplan mit Regeln

Stellen Sie sich einen Dienstplan für ein Wochenende vor. Für jede Frage entscheiden Sie nur mit Ja oder Nein: Arbeitet Anna am Samstag? Arbeitet Ben am Sonntag? Springt Cem für die Spätschicht ein? Alle Antworten zusammen sind ein Plan.

Dazu kommen Regeln. Jede Regel verlangt, dass von drei Aussagen mindestens eine stimmt, etwa: „Anna arbeitet am Samstag, oder Ben arbeitet nicht am Sonntag, oder Cem springt ein.“ Stimmt keine der drei, ist die Regel verletzt. Ein Plan ist gut, wenn keine Regel verletzt ist.

Manchmal gibt es keinen guten Plan, dann ist die Aufgabe unlösbar. Die Frage „Gibt es einen guten Plan?“ heißt bei Fachleuten SAT, nach dem englischen Wort für „erfüllbar“. Zwei Wege suchen einen guten Plan, und sie arbeiten gegensätzlich.

Weg 1: Umstellen, bis es passt

Sie raten zuerst einen ganzen Plan, etwa mit einer Münze für jede Frage. Er verletzt meist einige Regeln. Dann wiederholen Sie: Sie suchen sich eine verletzte Regel aus, nehmen eine ihrer drei Aussagen und kehren sie um, aus Ja wird Nein oder umgekehrt. Damit ist diese Regel erfüllt.

Der Haken: Die Umkehrung kann eine andere Regel verletzen, die bisher nur durch genau diese Aussage gehalten hat. Deshalb prüfen Sie bei jeder der drei Aussagen, wie viele andere Regeln beim Umkehren brechen würden, und wählen zufällig, mit Vorliebe die mit dem geringsten Schaden. Auch eine Aussage mit Schaden kann gewählt werden. Der Plan wird dann kurzfristig schlechter.

Dieser Weg führt kein Buch über frühere Versuche, und er liefert keinen Beweis. Findet er bis zu einer festen Obergrenze an Umstellungen keinen guten Plan, lautet die Antwort „weiß ich nicht“, nicht „gibt es nicht“. Fachleute nennen das lokale Suche.

Weg 2: Aufbauen und Notizen machen

Hier legen Sie die Antworten Frage für Frage fest und prüfen nach jeder, was daraus zwingend folgt. Läuft es in eine Sackgasse, verletzt also jede Fortsetzung eine Regel, fragen Sie: Welche Festlegungen haben das verursacht? Daraus schreiben Sie eine neue Regel auf, etwa „Diese Kombination geht nicht“. Dann springen Sie so weit zurück, bis die neue Regel eine Antwort erzwingt.

Mit der Zeit wächst ein Notizbuch aus Regeln. Es soll verhindern, dieselbe Sackgasse noch einmal zu betreten. Widersprechen sich die Notizen irgendwann, steht fest: Einen guten Plan gibt es nicht. Dieser Weg kann also beweisen, dass es nicht geht. Fachleute nennen ihn Konfliktlernen.

Zufällige Regeln: Je größer die Aufgabe, desto besser das Umstellen

Nun zählen wir, wie viel Arbeit beide Wege brauchen. Ein Lesezugriff ist wie ein Blick in die Regelliste, um etwas nachzuschlagen: Wer weniger nachschlägt, hat weniger gearbeitet. Beide Wege schlagen allerdings Verschiedenes nach, die Zahlen sind nur grob vergleichbar. Minuten wurden nicht gemessen.

Als typischen Wert nehmen wir den Median, den mittleren Wert: Hätten fünf Aufgaben geklappt, wäre es die drittkleinste Arbeit. Aufgaben, die ein Weg nicht löst, zählen dabei nicht mit. Ein Weg, der nur die leichten schafft, sieht darum besser aus, als er ist.

Jetzt hat der Plan nicht drei, sondern viele Fragen: Bei 100 Fragen sind es 100 Ja-Nein-Entscheidungen, und die Regeln wurden zufällig gewürfelt, rund vier Regeln je Frage. Jeder Weg durfte nur bis zu einer festen Obergrenze probieren. Das Umstellen zählt als erfolgreich, wenn mindestens einer von 3 Versuchen mit anderem geratenem Anfangsplan klappte. Die Tabelle nennt, wie viele von 12 Aufgaben je Größe gelöst wurden.

Fragen im Plan	Weniger Lesezugriffe	Gelöst von 12: Notizen	Gelöst von 12: Umstellen
100	Notizen (bei etwas mehr Regeln je Frage)	12	12
150	Umstellen	12	12
300	Umstellen	7	12
600	kein Vergleich: Notizen lösten keine	0	12

Ab 150 Fragen wird der Vorsprung des Umstellens also größer, bei 100 Fragen war es umgekehrt. Mit anderen Aufgaben je Größe schwankten die Zahlen, die Richtung blieb.

Eng verflochtene Regeln: Die Notizen gewinnen

Anders ist es, wenn die Regeln eng ineinandergreifen. Beispiel: Lieferaufträge sollen auf 3 Rampen verteilt werden, und Aufträge, die miteinander in Konflikt stehen, dürfen nicht an dieselbe Rampe. Gemessen wurden feste Aufgaben dieser Art, lösbare und unlösbare gemischt.

Das Umstellen fand nicht in jedem Versuch einen Plan. Wenn es gelang, brauchte es typisch 34-mal so viele Lesezugriffe wie der Weg mit Notizen, also viel mehr Nachschläge, nicht 34-mal so viele Minuten. Der Median steht dabei nur über die gelösten Fälle.

In einer weiteren eng verflochtenen Aufgabe, die der Fachteil beschreibt, löste das Umstellen nur 3 von 20 Versuchen, der Weg mit Notizen löste sie. Das ist eine einzige Aufgabe, also nur ein Hinweis.

Warum das so ist, wurde nicht gemessen. Eine Deutung: Hängen die Regeln eng zusammen, reißt jede Umstellung leicht eine andere Regel auf, ohne dass man dem Ziel näher kommt. Ein Notizbuch hält fest, was sich nicht verträgt.

Nur ein Weg kann „geht nicht“ sagen

Ein Beispiel zum Nachzählen: Drei Ja-Nein-Fragen haben acht mögliche Pläne. Nehmen wir acht Regeln, die je genau einen dieser Pläne verbieten. Dann verletzt jeder Plan genau eine Regel, und es gibt keinen guten Plan.

Der Weg mit Notizen meldete nach 4 Sackgassen: unlösbar. Das Umstellen kam bis zur Obergrenze nicht unter eine verletzte Regel. Es kann nicht erkennen, dass es nicht besser geht, es kann nur weitermachen.

Das zeigte sich in allen Messungen: Wo der Weg mit Notizen bewies, dass es keinen guten Plan gibt, fand das Umstellen keinen, und das ist folgerichtig, denn es sucht nur einen Plan ohne verletzte Regel. Der Weg mit Notizen kann bei großen Aufgaben an der Obergrenze scheitern, dann sagt auch er „unbekannt“.

Wann welchen Weg wählen?

Als Faustregel aus diesen Messungen, nicht als Gesetz: Bei zufällig gewürfelten Regeln und großen Aufgaben lohnt zuerst das Umstellen, bei eng verflochtenen Aufgaben das Notizbuch. Brauchen Sie die Gewissheit „geht nicht“, bleibt nur das Notizbuch. Ob Ihre Aufgabe zufällig oder verflochten ist, zeigt erst ein Versuch.

Häufige Missverständnisse

• „Wer gewinnt, gewinnt überall.“ Nein. In den Messungen gewann das Umstellen bei Zufallsregeln mit wachsender Größe, verlor aber bei den gemessenen eng verflochtenen Aufgaben und kann nicht „geht nicht“ sagen.
• „Findet das Umstellen nichts, gibt es nichts.“ Nein. Es heißt nur „weiß ich nicht“. Bei einzelnen Aufgaben gelang es in einem Versuch und im nächsten nicht.
• „Weniger Lesezugriffe heißt schneller.“ Nein. Minuten wurden nicht gemessen.

Woran Sie das im Alltag erkennen

• Sie schieben einen Plan hin und her, jede Reparatur reißt woanders ein Loch auf, und nach einer Weile stehen Sie wieder bei einem früheren Zustand. Das spricht für eine eng verflochtene Aufgabe: Zeit für ein Notizbuch, welche Kombinationen sich nicht vertragen.

Wie ernst ist das Rechenbild zu nehmen?

Gemessen wurden Ja-Nein-Fragen mit Regeln aus drei Aussagen, zwei Verfahren in lesbarem Programmcode und je eine Einstellung. Ob schnelle Programme der Praxis beide Wege verbinden, sagt diese Seite nicht.

Was Sie mitnehmen

• Ein Plan, der sich durch Umstellen nicht beruhigt, ist noch kein unlösbarer Plan: Nur Notizen mit Gründen können „geht nicht“ beweisen.
• Fragen Sie bei „nicht gelöst“ nach der Obergrenze: Nicht gefunden heißt nicht unlösbar.

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

Gegeben ist eine Formel in konjunktiver Normalform mit den Klauseln \(C_1, \dots, C_m\) über den Variablen \(x_1, \dots, x_n\), meist mit drei Literalen je Klausel (3-KNF). Gesucht ist eine Belegung \(\beta \in \{0, 1\}^n\), die jede Klausel erfüllt (ein Modell), oder der Nachweis, dass es keine gibt. Verglichen werden zwei Verfahren mit demselben Zweck und entgegengesetzter Bauweise.

• probSAT (stochastische lokale Suche): Start mit einem Münzwurf je Variable. Solange eine Klausel verletzt ist, wird eine verletzte Klausel gleichverteilt gezogen und aus ihr eine Variable mit Wahrscheinlichkeit proportional zu \((\varepsilon + \mathrm{break})^{-c_b}\) umgedreht. Kein Make-Anteil, kein Neustart, kein Gedächtnis. Voreinstellung \(c_b = 2{,}3\) nach Balint und Schöning (SAT 2012; für 3-SAT ohne Make-Anteil, Volltext gelesen) und \(\varepsilon = 0{,}9\) (Voreinstellung der hier verwendeten Fassung; das Papier verwendet nach der Prüfung am Preprint \(\varepsilon = 1\), die Wirkung von \(\varepsilon\) ist nicht gemessen).
• CDCL (Konfliktlernen): eigene Fassung mit 1-UIP-Konfliktanalyse, Aktivität der Variablen, Phasenspeicher, Luby-Neustarts und Watched Literals; Konfliktbudget 20.000 in den vorgerechneten Messreihen. CDCL antwortet erfüllbar, unerfüllbar oder (am Budget) unbekannt; probSAT antwortet Modell oder unbekannt, nie unerfüllbar.
• Aufwand: Literal-Lesezugriffe. Bei CDCL zählen die gelesenen Literale der Propagation und der Konfliktanalyse, bei probSAT \(3m\) beim Füllen der Zähler, je Umdrehung die Vorkommen der wahren Literale der drei Variablen (Break-Zählung) und die Vorkommen beider Literale der umgedrehten Variablen. Das sind Zählgrößen verschiedener Operationen, nur der Größenordnung nach vergleichbar. Ein Median steht nur über die gelösten Fälle eines Verfahrens und ist eine untere Schranke seiner Kosten, sobald Fälle ungelöst bleiben.
• Instanzen (Zufallszahlen aus dem ganzzahligen Generator SplitMix64, auf jeder Plattform gleich): Zufalls-3-SAT mit \(n = 100, 150, 300, 600\) und \(m/n = 4{,}0\) / \(4{,}2\) / \(4{,}26\) (der letzte Wert im Übergangsbereich); Aufträge auf Rampen als 3-Färbung eines Konfliktgraphen (160 Aufträge, mittlerer Grad 4,5, 3 Rampen); Schur-Partitionen \(k = 4,\ n = 43\) und \(k = 3,\ n = 13\) (Zahlen \(1, \dots, n\) auf \(k\) Mengen, keine Menge enthält \(a + b = c\), auch \(a = b\)); das Schubfachprinzip mit \(h = 5\) Löchern (6 Tauben, 30 Variablen, 81 Klauseln) als unerfüllbarer Fall.

Die Formeln

Aus einer gleichverteilt gezogenen verletzten Klausel \(C\) mit den Variablen \(v_1, v_2, v_3\) wird eine Variable umgedreht. Für die aktuelle Belegung \(\beta\) und eine Variable \(x_v\) ist der Schaden des Umdrehens ihr Break, die Zahl der Klauseln \(C_j\), die nur durch das aktuell wahre Literal von \(x_v\) erfüllt sind:

\[\mathrm{break}(v) = \bigl|\{\, C_j : \text{das aktuell wahre Literal von } x_v \text{ ist das einzige wahre Literal von } C_j \,\}\bigr|\]

Mit den Parametern \(\varepsilon\) und \(c_b\) bekommt jede der drei Variablen ein Gewicht \(w_v\), und gewählt wird \(v\) mit der Wahrscheinlichkeit \(P(v)\):

\[w_v = (\varepsilon + \mathrm{break}(v))^{-c_b}, \qquad P(v) = \frac{w_v}{w_{v_1} + w_{v_2} + w_{v_3}}\]

Umgesetzt wird die Wahl mit einer gleichverteilten Zufallszahl \(u\) in \([0, 1)\): gewählt wird das erste Literal, dessen kumulierte Gewichtssumme mindestens \(u\) mal die Gesamtsumme beträgt:

\[k^{*} = \min \Bigl\{\, k : \sum_{i \le k} w_{v_i} \ge u \cdot \sum_{i \le 3} w_{v_i} \Bigr\}\]

Handbeispiel (Schritt 0, Zufalls-Seed 20): Die Belegung ist 00000, verletzt ist nur \(C_1 = (x_1 \lor x_2 \lor x_3)\). Die Break-Werte sind \(0, 1, 1\), also mit \(\varepsilon = 0{,}9\) und \(c_b = 2{,}3\):

\[w = (0{,}9^{-2{,}3},\; 1{,}9^{-2{,}3},\; 1{,}9^{-2{,}3}) \approx (1{,}2742,\; 0{,}2285,\; 0{,}2285)\]

Das Handbeispiel hat \(n = 5\) Variablen und 7 Klauseln, 9 Modelle von 32 Belegungen; nach 3 Umdrehungen ist das Modell 10000 erreicht, die Lesezugriffe sind 32 / 44 / 54.

Herleitung: was die Gewichtung bewirkt

Dreht man eine Variable einer verletzten Klausel um, wird diese Klausel erfüllt. Die Zahl der verletzten Klauseln ändert sich dabei um \(\mathrm{break}(v) - \mathrm{make}(v)\), mit \(\mathrm{make}(v) \ge 1\), wobei \(\mathrm{make}(v)\) die Zahl der verletzten Klauseln ist, die das Umdrehen erfüllt. Die Gewichtung dieser Demo benutzt nur den Break-Anteil.

• Je kleiner der Break, desto größer das Gewicht \(w_v\); der Parameter \(c_b\) bestimmt, wie stark Umdrehungen ohne Schaden bevorzugt werden, \(\varepsilon\) verhindert ein unendliches Gewicht bei \(\mathrm{break}(v) = 0\).
• Gezogen wird mit Wahrscheinlichkeit proportional zum Gewicht, also auch eine Variable mit \(\mathrm{break}(v) > 0\): Verschlechterungen sind möglich. Im Handbeispiel ist das Gewicht der Variablen mit Break 0 gegenüber einer mit Break 1 um den Faktor 5,6 größer, ihre Wahrscheinlichkeit beträgt \(P = 73{,}6\) %.
• Bei einer unerfüllbaren Formel bleibt \(\min_\beta |\{\text{verletzte Klauseln}\}| \ge 1\): Eine Belegung ohne verletzte Klausel gibt es nicht, die Antwort bleibt „unbekannt“.

Befunde

Zufallsformeln: je Zelle 12 feste Formeln (Zufalls-Seeds 8000 bis 8011 der Formelerzeugung), je Formel 3 probSAT-Läufe (Zufalls-Seeds 1 bis 3, also 36 Läufe je Zelle), \(c_b = 2{,}3\), \(\varepsilon = 0{,}9\), Budgets 300.000 Umdrehungen (probSAT) und 20.000 Konflikte (CDCL, ein Lauf je Formel). „Offen“ heißt: CDCL hat im Konfliktbudget weder ein Modell gefunden noch Unerfüllbarkeit bewiesen. Mediane der Lesezugriffe stehen nur über die gelösten Fälle des Verfahrens.

\(n\) bei \(m/n = 4{,}0\)	CDCL: Modell gefunden (von 12 Formeln)	probSAT: Formeln in mindestens einem Lauf gelöst	probSAT: gelöste Läufe (von 36)
100	12	12	36
150	12	12	36
300	7 (5 offen)	12	35
600	0 (12 offen)	12	35

Im Übergangsbereich entscheidet CDCL bei \(n = 100\) und \(150\) alle 12 Formeln: bei \(m/n = 4{,}2\) sind 6 erfüllbar und 6 unerfüllbar (beide \(n\)), bei \(4{,}26\) 6 und 6 (\(n = 100\)) bzw. 4 und 8 (\(n = 150\)). probSAT löst dort genau die von CDCL als erfüllbar gefundenen Formeln, in allen drei Läufen, und keine unerfüllbare. Bei \(n = 300\) findet CDCL nur 1 Formel (11 offen, bei beiden Verhältnissen), probSAT löst 25 bzw. 18 von 36 Läufen (9 bzw. 6 Formeln); bei \(n = 600\) entscheidet CDCL keine Formel, probSAT löst 21 bzw. 12 von 36 Läufen (9 bzw. 6 Formeln).

Verhältnis der Mediane der Lesezugriffe, CDCL zu probSAT (größer als 1: probSAT braucht weniger):

\(n\)	\(m/n = 4{,}0\) / \(4{,}2\) / \(4{,}26\)	Vorbehalt
100	1,5 / 0,4 / 0,5	bei 4,2 und 4,26 braucht probSAT das 2,7- bzw. 2,2-Fache von CDCL
150	2,6 / 5,5 / 1,8	beide Verfahren lösen dieselben Formeln
300	33 / 69 / 61	bei 4,2 und 4,26 stammt der CDCL-Median aus je einem gelösten Fall (untere Schranke seiner Kosten), der probSAT-Median aus 25 bzw. 18 von 36 Läufen: nur ein Richtwert; bei 4,0 stehen 7 CDCL-Werte und 35 von 36 probSAT-Läufen dahinter
600	kein CDCL-Median	CDCL löst im Budget keine Formel

Das Verhältnis mischt Instanzmengen: Jedes Verfahren hat seinen Median über die eigenen gelösten Fälle; bei \(n = 100\) und \(150\) sind das dieselben Formeln, bei \(n = 300\) nicht. Eine Gegenprobe mit anderen zwölf Formeln (Zufalls-Seeds 9000 bis 9011, \(n = 150\) und \(300\), sonst gleiche Verfahren und Budgets) reproduziert die Richtung: Bei \(n = 150\) ist probSAT in allen drei Verhältnissen günstiger (Faktor 5,1 / 10,2 / 4,6, in der Hauptreihe 2,6 / 5,5 / 1,8), bei \(n = 300\) löst CDCL höchstens 3 von 12 Formeln, probSAT 36 / 30 / 19 von 36 Läufen. Die Zahlen schwanken mit der Formelmenge: CDCL findet bei \(n = 300\), \(m/n = 4{,}0\) in der Hauptreihe 7, in der Gegenprobe 3 Formeln, und der Anteil unerfüllbarer Formeln bei \(n = 150\), \(m/n = 4{,}26\) ist 8 von 12 gegen 4 von 12. Die Reihenfolge „bei \(n = 100\) ist CDCL günstiger, ab \(n = 150\) probSAT“ ist deshalb nur für die Hauptreihe belegt, \(n = 100\) steht nicht in der Gegenprobe.

Gleiche Formel, anderer Zufalls-Seed: Bei 11 der 144 Zufallsformeln gelang nur ein Teil der drei Läufe, davon 9 bei \(n = 600\) (1 / 4 / 4 bei \(m/n = 4{,}0\) / \(4{,}2\) / \(4{,}26\)) und 2 bei \(n = 300\). Beispiel: \(n = 300\), \(m/n = 4{,}2\), Formel mit Zufalls-Seed 8008: Zufalls-Seed 3 findet nach 27.426 Umdrehungen ein Modell, die Zufalls-Seeds 1 und 2 nicht in 300.000. Robustheit gegen \(c_b\): Mit \(c_b = 2{,}06\) statt \(2{,}3\) (dieselben Formeln und Zufalls-Seeds, nur \(n = 300\) und \(600\)) weicht die Zahl gelöster Läufe in keiner der sechs Zellen um mehr als einen Lauf ab (36 / 25 / 18 bei \(n = 300\), 34 / 20 / 11 bei \(n = 600\) gegen 35 / 25 / 18 und 35 / 21 / 12); die Mediane der probSAT-Läufe unterscheiden sich, zum Beispiel bei \(n = 300\), \(m/n = 4{,}26\): 991.560 gegen 728.636.

Struktur: CDCL gegen probSAT, Median der Lesezugriffe über die gelösten Fälle (probSAT mit \(c_b = 2{,}3\) und \(\varepsilon = 0{,}9\), Budget 300.000 Umdrehungen, CDCL 20.000 Konflikte):

Aufgabe	CDCL	probSAT	Verhältnis, Vorbehalt
Rampen: 10 feste Konfliktgraphen (Zufalls-Seeds 500 bis 509), 160 Aufträge, 3 Rampen, mittlerer Grad 4,5	6 erfüllbar, 4 unerfüllbar (Zufalls-Seeds 501, 504, 505, 509); Median 27.570,5 (6 Werte)	23 von 30 Läufen auf den 6 erfüllbaren Graphen (5 Läufe je Graph), keiner auf den unerfüllbaren; Median 929.074 (23 Werte)	34-mal mehr für probSAT
Schur \(k = 4,\ n = 43\): eine Instanz, 20 Läufe	2.835 (1 Wert)	12.842.630, 3 von 20 Läufen gelöst	4530-mal mehr für probSAT, untere Schranke
Schur \(k = 3,\ n = 13\)	1.276	22.297 (20 von 20 Läufen)	17-mal mehr für probSAT
Lateinisches Quadrat, Ordnung 12, Lücken 0,58, 4 Instanzen	löst alle 4	0 von 20 Läufen	eingefrorene Konstante einer Vormessung (andere Instanzfamilie, Zufallsgenerator Python-random, \(c_b = 2{,}06\)), nicht nachgerechnet

Unerfüllbare Formeln:

Fall	CDCL	probSAT
Zufallsformeln \(n = 150\), \(m/n = 4{,}26\) (12 Formeln)	beweist 8 von 12 als unerfüllbar	kein Modell in den 24 Läufen auf diesen Formeln
alle 8 Klauseln über 3 Variablen	nach 4 Konflikten „unerfüllbar“	nach 1.000 Umdrehungen kleinste Zahl verletzter Klauseln 1 (jede der 8 Belegungen verletzt genau eine)
Schubfach \(h = 5\) (30 Variablen, 81 Klauseln)	nach 159 Konflikten „unerfüllbar“	nach 300.000 Umdrehungen (Zufalls-Seed 20) kleinste Zahl 1
unerfüllbare Färbung (Graph mit Zufalls-Seed 501, 480 Variablen, 1.240 Klauseln)	nach 151 Konflikten „unerfüllbar“	nach 300.000 Umdrehungen (Zufalls-Seed 20) kleinste Zahl 1

Über alle 144 Zufallsformeln und die Strukturinstanzen löst probSAT keine von CDCL als unerfüllbar bewiesene Formel.

Grenzen: was die Messung zeigt und was nicht

• Eine Gewichtung, ein Verfahren. Gemessen ist probSAT mit der polynomiellen Gewichtung ohne Make-Anteil und ohne Neustart an 3-SAT-Familien. Für 5-SAT und 7-SAT nennt das Papier eine andere Gewichtung als bessere. „Die lokale Suche gewinnt bei Zufallsformeln“ gilt nur für die gemessenen Zellen (\(n = 150\) bis \(600\), \(m/n = 4{,}0\) bis \(4{,}26\)) und diese Gewichtung; bei \(n = 100\) und \(m/n = 4{,}2\) bis \(4{,}26\) sagt die Messung das Gegenteil.
• Wenige Formeln. 12 feste Formeln je Zelle, 10 Konfliktgraphen, bei Schur eine Instanz; die Gegenprobe zeigt Schwankungen. Ein Median über die Gelösten ist eine untere Schranke der Kosten, sobald Fälle ungelöst bleiben; das betrifft \(n = 300\) mit \(m/n = 4{,}2\) und \(4{,}26\) (ein CDCL-Wert) und beide Schur-Instanzen (ein CDCL-Wert).
• Budgets verschiedener Einheiten. 300.000 Umdrehungen gegen 20.000 Konflikte; „offen“ heißt bei CDCL nur „im Budget nichts entschieden“. Mit anderen Budgets verschieben sich die Zahlen gelöster Fälle.
• Zählgrößen statt Zeit. Lesezugriffe zählen verschiedene Operationen und sind nur der Größenordnung nach vergleichbar; Zeit ist nicht gemessen, beide Verfahren laufen als lesbarer Python-Code. Aussagen über optimierte Löser in C sind nicht möglich.
• Keine Hybride. Ob moderne Löser CDCL und lokale Suche verbinden, steht in keiner der gelesenen Quellen und wird nicht behauptet; gezeigt sind zwei getrennte Verfahren.
• Ein Lauf ohne Lösung beweist nichts. Wie viele Läufe nötig sind, um eine erfüllbare Formel „fast sicher“ zu lösen, ist nicht gemessen.
• Parameter. Die Wirkung von \(\varepsilon\) ist nicht gemessen, ebenso nicht die von \(c_b\) außer der Gegenüberstellung 2,06 gegen 2,3. Die Zeile zu lateinischen Quadraten ist eine eingefrorene Konstante.
• Deutungen. Die Messung zeigt, wo welches Verfahren weniger zählt, nicht warum; Sätze zum Warum sind Deutungen.

Erweiterungen und Verweise

Nicht umgesetzt sind andere Verfahren der lokalen Suche (WalkSAT-Varianten, Sparrow, Neustarts, Tabu), Hybride mit Phasen aus lokaler Suche, Zeitmessungen und Industrieinstanzen. Verwandte Seiten:

• Zufallsformeln, DPLL-Suche und der Übergang der Erfüllbarkeit: Der Phasenübergang bei SAT verständlich erklärt.
• Dieselbe Idee „kleine Änderung, Verschlechterung erlaubt“ an Routen: Trajektorien-Metaheuristiken.

Quellen

• Balint, A. und Schöning, U.: Choosing probability distributions for stochastic local search and the role of make versus break. SAT 2012, LNCS 7317, S. 16–29.

Aus der README der Demo übernommen (dort ist der Volltext als gelesen vermerkt); auf dieser Seite nicht neu nachgeschlagen. Weitere Literatur wurde nicht herangezogen.