New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09],...

99
Schwere Instanzen für NP -schwere Probleme Hard instances for NP -hard problems Masterarbeit im Rahmen des Studiengangs Informatik der Universität zu Lübeck vorgelegt von Tobias Schomann ausgegeben und betreut von Prof. Dr. math. Rüdiger Reischuk Lübeck, den 18. September 2015

Transcript of New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09],...

Page 1: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Schwere Instanzen für NP-schwere Probleme

Hard instances for NP-hard problems

Masterarbeit

im Rahmen des StudiengangsInformatikder Universität zu Lübeck

vorgelegt vonTobias Schomann

ausgegeben und betreut vonProf. Dr. math. Rüdiger Reischuk

Lübeck, den 18. September 2015

Page 2: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut
Page 3: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Erklärung

Hiermit versichere ich an Eides statt, durch meine Unterschrift, dass ich die vorliegende Arbeitselbstständig verfasst und keine anderen als die angegebenen Quellen und Hilfsmittel benutzt habe.

Ort, Datum Unterzeichner

Page 4: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut
Page 5: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kurzzusammenfassung

In dieser Arbeit wurden randomisierte Methoden zur Konstruktion von garantiert erfüllbaren, aus-sagenlogischen Formeln ausgearbeitet. Eine neu vorgestellte Methode basiert auf dem Ansatz, dieKlauseln einer gegebenen, festen Formeln in konjunktiver Normalform zu vervielfältigen und dieLiterale innerhalb der Kopien randomisiert zu vertauschen, so dass beleibig große Formeln gene-riert werden können. Weitere Konstruktionsverfahren basieren auf NP-vollständigen Problemen,wie Graph-Färbbarkeit, Hypergraph-Färbarkeit, Problem der exakten Überdeckung und Teilgraph-Isomorphie. Auf diese Weise konstruierte Formeln wurden mit Hilfe verschiedener SAT-Solverexperimentell untersucht. Ein SAT-Algorithmus von Schöning wurde im Rahmen dieser Arbeitimplementiert, weitere SLS- (Stochastic Local Search) und DPLL-basierte (Davis, Putnam, Lo-geman, Loveland) Solver, die im Rahmen der SAT Competetion 2011 veröffentlich wurden, sindeingesetzt worden. Es wurden Eigenschaften der Formeln wie Zeitaufwand der Solver und Anzahlder erfüllenden Belegungen in Abhängigkeit der Formelnparameter untersucht. Die Ergebnissezeigen unter anderem, dass die SAT-Solver durch Vervielfältigung erzeugten Formeln exponenti-ellen Zeitaufwand zur Festellung der Erfüllbarkeit benötigen.

Abstract

In this work randomized methods for construction of guaranteed satisfiable, propositional logicformulas have been elaborated. A new presented method is based on the approach to reproduceclauses of a given fixed formula in conjunctive normal form and to swap the literals inside thecopies randomly, so that can be generated arbitrarily large formulas. Other methods of constructi-on are based onNP-complete problems such as graph colorability, hypergraph colorability, exactcover and subgraph isomorphism. Formulas, which were constructed in this way, were investiga-ted experimentally, by using different SAT-solvers. In the context of this work a SAT-algorithmby Schöning was implemented, other SLS- (Stochastic Local Search) and DPLL-based (Davis,Putnam, Logeman, Loveland) solvers, which were published in the context of SAT Competition2011, have been used. Properties of the formulas, as running time of solvers and number of satis-fying assignments, depending on the formula parameters, were examined. The results in this workshow among others, that the SAT-solvers need exponential time, to determine satisfiability of theformulas, which were generated by duplication.

Page 6: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut
Page 7: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Inhaltsverzeichnis

1 Einleitung 9

1.1 Aufbau der Arbeit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2 NP-vollständige Probleme 13

2.1 Graphentheorie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2.2 Färbbarkeit von Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

2.3 Cliquenproblem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

2.4 Problem der exakten Überdeckung . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.5 Teilgraph-Isomorphie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.6 Erdos Diskrepanzprobleme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3 Aussagenlogik und SAT-Solving 19

3.1 Aussagenlogik . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3.2 SAT-Solver . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

3.3 DPLL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

3.4 Stochastic Local Search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

3.5 Random Walk von Schöning . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

3.6 Ein Verfahren basierend auf Message-Passing . . . . . . . . . . . . . . . . . . . 30

3.7 Conflict Driven Clause Learning . . . . . . . . . . . . . . . . . . . . . . . . . . 30

3.8 Vorstellung von implementierten SAT-Solvern . . . . . . . . . . . . . . . . . . . 31

4 Konstruktion von SAT-Formeln 35

4.1 Reduktion von Graph-Färbbarkeit . . . . . . . . . . . . . . . . . . . . . . . . . 35

4.2 Reduktion von Hypergraph-Färbbarkeit . . . . . . . . . . . . . . . . . . . . . . 37

4.3 Reduktion von X3C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

7

Page 8: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

4.4 Reduktion von Teilgraph-Isomorphie . . . . . . . . . . . . . . . . . . . . . . . . 40

4.5 Reduktion von EDP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42

4.6 Vervielfältigung von Klauseln . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

4.7 Zufällige Formeln in 3-KNF . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

5 Experimentelle Untersuchungen 47

5.1 Implementierung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47

5.2 Testumgebung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

5.3 Auswertung der Testdaten . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48

5.4 Vervielfältigung einer festen 3-SAT Formel . . . . . . . . . . . . . . . . . . . . 49

5.5 3-Färbbarkeit von Graphen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

5.6 3-Färbbarkeit von 3-uniformen Hypergraphen . . . . . . . . . . . . . . . . . . . 61

5.7 Das X3C-Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67

5.8 Teilgraph-Isomorphie . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

5.9 Vergleich der Formelfamilien . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77

6 Abschlussdiskussion und Ausblick 81

6.1 Offene Fragen . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84

A Anhang 87

A.1 Basisformel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87

A.2 Inhalt der beigelegten CD . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88

A.3 Abbildungsverzeichnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

A.4 Tabellenverzeichnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

A.5 Algorithmenverzeichnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95

A.6 Literaturverzeichnis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97

8

Page 9: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 1

Einleitung

Die Informatik ermöglicht uns heutzutage, schnell und mit hoher Zuverlässigkeit, Aufgaben zulösen, die aus menschlicher Sichtweise scheinbar eine hohe Komplexität besitzen. So ist es fürNavigationssysteme mit gewöhnlicher Hardwareausstattung kein Problem mehr, innerhalb vonwenigen Sekunden, die beste Route zwischen zwei Orten in einem komplizierten Netzwerk ausMillionen von Straßen zu finden. Solche und auch andere Beispiele des Alltags können den Ein-druck entstehen lassen, Computer könnten mittlerweile jede erdenkliche algorithmische Aufgabein kurzer Zeit lösen. Doch dieser Eindruck täuscht, es gibt in der Informatik Problemstellungen,die, sowohl für die Theorie, als auch für die Praxis eine hohe Relevanz haben, aber für die nochkeine effizienten Lösungsverfahren bekannt sind. Es ist bis heute nicht einmal geklärt, ob solcheVerfahren überhaupt existieren. Eine besonders wichtige Klasse solcher algorithmischen Problemeist die der NP-vollständigen Probleme.

Das Erfüllbarkeitsproblem der Aussagenlogik ist das erste Problem dem nachgewiesen wurde,dass es NP-vollständig ist. Stephen Cook hat mit seinem „Satz von Cook“, wie wir ihn heutenennen, im Jahr 1971 diesen Beweis erbracht und gleichzeitig Begriffe wie P , NP , NP-schwer,NP-vollständig und so fort eingeführt [COO71]. Das SAT-Problem, wie das Erfüllbarkeitspro-blem in Anlehnung an den englischen Begriff Satisfiability auch genannt wird, ist in theoretischerund praktischer Hinsicht eines der wichtigsten algorithmische Problem der Informatik, daher wirdes manchmal auch als die Drosophila der Komplexitätstheorie bezeichnet (vergleiche [SCH10]).Nach 1971 folgten viele weitereNP-Vollständigkeitsbeweise, denn es war jetzt ein Vertreter die-ser Komplexitätsklasse bekannt und es reichte für ein Problem inNP daher aus, einen effizientenAlgorithmus anzugeben, der das Problem SAT in das Zielproblem überführt: eine sogenannte Po-lynomialzeitreduktion.

Da nun alle Probleme in NP , somit auch die NP-vollständigen, effizient in das SAT-Problemüberführt werden können, würde die Existenz eines effizienten Algorithmus für dieses Problembewirken, dass alle Probleme in NP effizient lösbar wären. Darum ist es das erklärte Ziel vie-ler Informatiker, immer bessere SAT-Algorithmen zu entwickeln, auch wenn ein Polynomialzeit-Algorithmus derzeit unerreichbar scheint. Einige dieser hochgradig optimierten Lösungverfahren,die man auch SAT-Solver nennt, wie zum Beispiel das DPLL-Verfahren oder Stochastic LocalSearch, werden in dieser Arbeit besprochen und vorgestellt.

In der Informatik kommt es oft vor, dass die Theorie der Praxis weit vorraus ist. So wurde zumBeispiel das theoretische Modell eines Computers, die Turing-Maschine, bereits untersucht noch

9

Page 10: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

bevor der erste Computer dieser Art gebaut wurde. Aber auch im Bereich der Quanteninformatikhaben wir diese Situation, dass die Theorie bereits weit fortgeschritten ist und viele Erkenntnissegesammelt hat, die vermutlich einmal von großem Nutzen (oder Schaden für Verschlüsselungsver-fahren) sein werden. Doch real exitierende Quantencomputer schaffen es gerade einmal, die Zahl143 zu faktorisieren [XU12]. Im Bereich des SAT-Solving sieht die Situation anders aus. Es gibtviele Vermutungen, die bisher nur experimentell bestätigt werden konnten, wie zum Beispiel derkritische Punkt m/n = 4,2, bei dem zufällige 3-SAT-Formeln mit n Variablen und m Klauselnvon „mit großer Wahrscheinlichkeit erfüllbar“ zu „mit großer Wahrscheinlichkeit nicht erfüllbar“übergehen. Auch die in der Praxis erreichten Laufzeiten der Solver gehen noch über das, was dieTheorie gesichert sagen kann, deutlich hinaus. Die Verbesserung der in SAT-Solvern eingesetztenHeuristiken geschieht daher oft auf experimenteller Basis, indem sie an verschiedenen Arten vonSAT-Formeln systematisch ausprobiert werden. Viele Forscher testen ihre Solver zum Beispielmit zufälligen Formeln an dem bereits genannten Schwellwert, um ihre Solver für den Average-Case zu optimieren. Aber je nach Einsatzgebiet kann es auch sinnvoll sein, andere Formeltypen zuAnalysezwecken zu verwenden. Sogenannte unvollständige SAT-Solver, die nur die Erfüllbarkeitvon erfüllbaren Formeln, nicht aber die Unerfüllbarkeit von unerfüllbaren Formeln sicher erken-nen können, benötigen daher Formeln, die auf der einen Seite garantiert erfüllbar sind, aber aufder anderen Seite diese Tatsache möglichst gut verschleiern. Ein Hauptthema dieser Arbeit ist dieVorstellung und Analyse randomisierter Konstruktionsverfahren von schweren SAT-Formeln, diegarantiert erfüllbar sind.

1.1 Aufbau der Arbeit

In der vorliegenden Arbeit wurden, auf Basis verschiedener NP-vollständiger Probleme, Metho-den zur Konstruktion von aussagenlogischen Formeln herausgearbeitet. Diese unterschiedlichenArten von Formeln wurden, hinsichtlich der Erfüllbarkeit, experimentell mit SAT-Solvern unter-sucht. Zunächst werden in Kapitel 2 daher einigeNP-vollständige Probleme definiert und Eigen-schaften dieser Probleme besprochen, die im weiteren Verlauf der Arbeit noch benötigt werden.

Im Kapitel 3 folgt dann, nach einer Einführung in die Aussagenlogik, die Vorstellung der wesent-lichen SAT-Solving-Verfahren. Für Schönings SAT-Algorithmus wurde hier eine ausführlichereAnalyse herausgearbeitet. Zum Schluss des Kapitels werden die, in der Arbeit verwendeten Im-plementierungen dieser Verfahren vorgestellt.

Mit Kapitel 4 beginnt der Hauptteil der Arbeit. Hier wurden verschiedene randomisierte Verfahrenzur Konstruktion von aussagenlogischen Formeln, die garantiert eine erfüllende Belegung besit-zen, ausgearbeitet. Sehen wir einmal von dem neu vorgestellten Verfahren in Abschnitt 4.6 ab,basieren diese Verfahren auf den in Kapitel 2 vergestellten NP-vollständigen Problemen.

In Kapitel 5 folgt die experimentelle Untersuchung dieser Formelfamilien mit den beschriebenenSAT-Solving-Verfahren. Hier werden für jeden Formeltyp in Abhängigkeit der Formelparameterverschiedene Aspekte, wie zum Beispiel asyptotische Laufzeit der Solver, Anzahl der erfüllendenBelegungen oder kitische Bereiche des Parameterraums, beleuchtet. Jeder Abschnitt in diesemKapitel enthält am Ende einen kurzen Überblick der gewonnenen Ergenisse. Zum Schluss desKapitels werden die unterschiedlichen Formeltypen miteinander verglichen.

Wir schließen den Haptteil der Arbeit und beginnen mit Kapitel 6 die abschließende Zusammen-fassung und Diskussion der Ergebnisse. Hier werden die wesentlichen Aspekte der Konstruktions-

10

Page 11: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

methoden noch einmal kurz erläutert und es werden die Ergebnisse und Intepretationen der expe-rimentellen Untersuchungen zusammenfassend dargestellt. Noch offene Fragestellungen werdenhier ebenfalls behandelt.

Im Anhang folgt, nach der Besprechung des Inhalts der beiliegenden CD, die Vorstellung eineraussagenlogischen Formel, die in dieser Arbeit eine wichtige Rolle spielt. Auf den letzten Seiten istein Abbildungsverzeichnis, Tabellenverzeichnis, Algorithmenverzeichnis und Literaturverzeichnisvorzufinden.

11

Page 12: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

12

Page 13: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 2

NP-vollständige Probleme

Da es durch Stephen Cooks Beweis aus dem Jahre 1971 [COO71] nun einen bekannten Vertreterder Komplexitätsklasse NP gab, war es jetzt möglich durch Polynomialzeitreduktionen weitereNP-vollständige Probleme zu finden. Karp nutzte diese Gelegenheit und zeigte bereits 1972 für21 Probleme der Informatik, die als besonders hartnäckig bekannt waren, dass diese ebenfallsNP-vollständig sind [KAR72].

In diesem Kapitel werden neben einigen theoretischen Grundlagen der Informatik auch bekannteProbleme vorgestellt, die NP-vollständig sind oder bei denen diese Eigenschaft zumindest ver-mutet wird.

Bibliographische Hinweise Als Grundlage für dieses Kapitel dienten unter anderem Introduc-tion to Algorithms von Thomas Cormen, Charles Leiserson, Ronald Rivest und Clifford Stein[COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12]und Hartmut Noltemeier und Random Graphs von Béla Bollobás [BOL01]. Weitere Quellen sindim Kapitel selbst aufgeführt.

2.1 Graphentheorie

Viele der Probleme, die in dieser Arbeit untersucht werden, sind Graphenprobleme oder eng ver-wand mit ihnen. Darum folgt nun eine Auswahl von Grundlagen und Erkenntnissen aus der Gra-phentheorie, die für diese Arbeit von Bedeutung sind. Wir betrachten in diesem Abschnitt aus-schließlich ungerichtete Graphen.

Definition 2.1 (Graph)Ein ungerichteter GraphG = (V,E) besteht aus einer abzählbaren Menge von Knoten V und eineMenge von Kanten E ⊆ {{i, j} | i, j ∈ V }.

Definition 2.2 (Hypergraph)Ein k-uniformer HypergraphG = (V,E) besteht aus einer abzählbaren Menge von Knoten V undeine Menge von Hyperkanten E ⊆ {{i1, i2, ..., ik} | i1, i2, ..., ik ∈ V }.

13

Page 14: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Bei der Analyse der späteren experimentellen Untersuchungen werden häufig Eigenschaften vonsogenannten Zufallsgraphen eine Rolle spielen. Darum werden wir nun zwei sehr häufig gebrauch-te Modelle von zufälligen Graphen kennenlernen. Ein Zufallsgraphenmodell ist dabei ein Wahr-scheinlichkeitsmaß auf einer Menge von Graphen.

• Das Modell G (n,M) besteht aus allen Graphen mit der Knotenmenge V = {1, 2, ..., n},die genau M Kanten haben. G (n,M) besteht aus

((n2)M

)Graphen, von denen jeder eine

Auftrittswahrscheinlichkeit von((n2)M

)−1hat.

• Das Modell G (n, p) besteht aus allen Graphen mit der Knotenmenge V = {1, 2, ..., n},bei denen jede Kante mit der Wahrscheinlichkeit p unabhängig von allen anderen Kantenexistiert. Analog hierzu haben wir die zufälligen k-uniformen Hypergraphen G (n, k, p).

Solche Zufallsgraphen sind schon lange Gegenstand intensiver Untersuchungen, die zu vielen In-teressanten Ergebnissen geführt haben. Einige Eignschaften von Zufallsgraphen werden hier nunaufgeführt. Die jeweiligen Beweise sind in entsprechenden Referenzen zu finden.

Satz 2.1 (Matula, 1976 [MAT76])Für n ≥ 1 und 0 > p > 1 gebe die Zufallsvariable Z(n, p) die Cliquenzahl des ZufallsgraphenG (n, p) an. Dann gilt für 1 ≥ k ≥ n k∑

j=max(0,2k−n)

(n−kk−j)(kj

)(nk

) p−j(j−1)

2

−1 ≤ Pr[Z(n, p) ≥ k] ≤(n

k

)p

k(k−1)2 .

Satz 2.2 (Erdos u. a., 1960 [ERD60])Sei G ∈ G (n, p) ein Zufallsgraph. Dann gilt:

• Wenn p > (1+ε) lnnn , dann ist G (fast) sicher zusammenhängend.

• Wenn p < (1−ε) lnnn , dann ist G (fast) sicher nicht zusammenhängend.

Satz 2.3 (Mulet u. a., 2002 [MUL02])Ein Zufallsgraph G ∈ G (n, p) mit pn > 4,69 ist fast sicher nicht 3-färbbar.

Satz 2.4 (Achlioptas u. a., 2002 [ACH02])Sei n, k ∈ N und p ∈ [0, 1]. Dann gilt für einen zufälligen Hypergraph H ∈H (n, p, k):

• Wenn p(nk

)≥ 2k−1 ln 2− ln 2

2 , dann ist H mit hoher Wahrscheinlichkeit nicht 2-färbbar.

• Wenn p(nk

)≤ 2k−1 ln 2− ln 2

2 − 1, dann ist H mit hoher Wahrscheinlichkeit 2-färbbar.

2.2 Färbbarkeit von Graphen

Eine Färbung eines ungerichteten Graphen weist jedem Knoten eine Farbe zu. Doch es wird zu-sätzlich verlangt, dass es sich dabei um eine sogenannte gültige Färbung handelt, also das niemalszwei benachbarte Knoten mit der gleichen Farbe gefärbt sind.

14

Page 15: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Definition 2.3 (Färbung)Sei ein ungerichteter Graph G = (V,E) und k ∈ N. Eine Abbildung c : V → {1, 2, ..., k} mitc(u) 6= c(v) für alle Kanten {u, v} ∈ E wird als k-Färbung des Graphen G bezeichnet.

Auf eine ähnliche Weise können wir die Färbbarkeit von Hypergraphen definieren. Für eine Hy-perkante wird dabei allerdings nur verlangt, dass nicht alle Knoten gleich gefärbt sind.

Definition 2.4 (Färbung)Sei ein q-uniformer Hypergraph H = (V,E) und k ∈ N. Eine Abbildung c : V → {1, 2, ..., k}wird als k-Färbung von H bezeichnet, wenn keine Hyperkante {v1, v2, ..., vq} ∈ E existiert, fürdie c(v1) = c(v2) = ... = c(vq) gilt.

Ausgehend von diesen Defninitionen ergeben sich nun die dazugehörigen Entscheidungsproble-me.

Definition 2.5 (Graph-Färbbarkeitsproblem)Die Menge der k-färbbaren Graphen wird durch k-COLORING bezeichnet. Die Frage, ob für einengegebenen Graph G gilt G ∈ k-COLORING, stellt das k-Färbbarkeitsproblem dar.

Das Hypergraph-Färbbarkeitsproblem lässt sich analog definieren, wir tauschen den Begriff Graphdurch q-uniformer Hypergraph aus.

Satz 2.5Das 3-Färbarkeitsproblem ist NP-vollständig.

Der Beweis zu dieser Aussage ist zum Beispiel in Introduction to Algorithms Seite 1103 zu finden[COR09]. Das nun folgende Ergebnis stammt aus der Arbeit [DIN05].

Satz 2.6Das Problem, eine k-Färbung für einen 3-uniformen 2-färbbaren Hypergraph anzugeben, istNP-schwer für eine Konstante k.

2.3 Cliquenproblem

Eine Eigenschaft eines Graphen, die in dieser Arbeit noch von Bedeutung sein wird, ist die Exis-tenz einer sogenannten Clique. In der Graphentheorie stellt eine Clique in einem Graph eine Teil-menge von Knoten dar, die untereinander vollständig verbunden sind. Das heißt, jeder Knoten derTeilmenge ist mit jedem anderen durch eine Kante verbunden. Es folgt nun eine formelle Defini-tion.

Definition 2.6 (Clique, Cliquenzahl)Sei ein ungerichteter Graph G = (V,E). Dann heißt eine Knotenteilmenge C ⊆ V Clique von G,wenn für alle i, j ∈ C auch {i, j} ∈ E gilt. Weiterhin heißt

ω(G) := max{|C| | C ist Clique von G}

die Cliquenzahl von G.

15

Page 16: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Das entsprechende Entscheidungsproblem, das k-Cliquenproblem, stellt die Frage ob in einemgegebenen Graphen eine Clique C der Größe |C| = k enthalten ist. Dieses Problem wird in dieserArbeit allerdings nicht weiter untersucht. Der Begriff der Clique ist aber bei der Analyse vonX3C-basierten SAT-Formeln hilfreich.

2.4 Problem der exakten Überdeckung

Definition 2.7 (Exakte Überdeckung)Sei eine Menge U . Dann ist eine Menge S ⊆ P (U) eine exakte Überdeckung von U , wenn diebeiden folgenden Aussagen gelten.

• Für alle Si, Sj ∈ S gilt: wenn Si 6= Sj , dann Si ∩ Sj = ∅ .

•⋃Si∈S

Si = U .

Mit Hilfe dieser Definition lässt sich nun einfach das entsprechende Entscheidungsproblem for-mulieren.

Definition 2.8 (Das Problem der exakten Überdeckung/Exact Cover Problem)Gegeben sei eine Grundmenge U und eine Menge S ⊆ P (U). Die Frage, ob eine TeilmengeS′ ⊆ S existiert, so dass S′ eine exakte Überdeckung für U ist, wird als Problem der exaktenÜberdeckung bezeichnet.

Satz 2.7Das Problem der exakten Überdeckung ist NP-vollständig.

Da das Problem der exakten Überdeckung eines von Karps 21 NP-vollständigen Problemen ist,kann der Beweis dieser Aussage in Karps Veröffentlichung aus dem Jahr 1972 [KAR72] gefundenwerden. Dort heißt das Problem Exact Cover.

Nun behandeln wir einen Spezialfall dieses Problems, der in dieser Arbeit noch genauer untersuchtwerden wird, das sogenannte X3C-Problem. Hier verlangen wir, dass die Menge S ausschließlichTripel enthält.

Definition 2.9 (X3C-Problem)Gegeben sei eine Grundmenge U und eine Menge S ⊆ P (U), wobei für alle Si ∈ S gilt |Si| = 3.Die Frage, ob eine Teilmenge S′ ⊆ S existiert, so dass S′ eine exakte Überdeckung für U ist,bezeichnet das X3C-Problem.

2.5 Teilgraph-Isomorphie

Nachfolgend werden ungerichtete Graphen mit endlicher Anzahl von Knoten und ohne Mehrfach-kanten betrachtet. Ein Graph G ist definiert als ein ein Paar G = (VG, EG), wobei VG eine Mengevon Knoten ist und EG ⊂ VG × VG eine Menge von Kanten. Die Anzahl der Knoten von einemGraph G wird durch nG bezeichnet und die Anzahl der Kanten durch mG.

16

Page 17: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Definition 2.10 (Teilgraph)Sei zwei Graphen G = (VG, EG) und H = (VH , EH). Dann ist G ein Teilgraph von H , wennVG ⊆ VH und EG ⊆ EH . Wenn zusätzlich EG = EG ∩ (VH × VH), dann wird G als induzierterTeilgraph bezeichnet.

Definition 2.11 (Graph-Isomorphie)Zwei GraphenG = (VG, EG) undH = (VH , EH) sind genau dann isomorph, wenn eine bijektiveAbbildung f : VG → VH existiert, so dass für alle v1, v2 ∈ VG mit v1 6= v2 gilt:

(v1, v2) ∈ EG ⇔ (f(v1), f(v2)) ∈ VH .

Definition 2.12 (Teilgraph-Isomorphie-Problem)Das Entscheidungsproblem, dass zu zwei gegebenen Graphen G und H die Frage stellt, ob G zueinem Teilgraph von H isomorph ist, wird als Teilgraph-Isomorphie-Problem bezeichnet.

Für das reine Graph-Isomorphie-Problem, bei dem wir zwei Graphen mit gleicher Knotenanzahlbetrachten, gehört zu den wenigen algorithmischen Problemen in NP , bei denen bis heute wederbekannt ist, ob sie in P liegen, noch ob sie NP-vollständig sind. Das gilt allerdings nicht für dasTeilgraph-Isomorphie-Problem.

Satz 2.8Das Teilgraph-Isomorphie-Problem ist NP-vollständig.

Der Beweis zu dieser Aussage ist bereits in der Arbeit enthalten, in der auch dieNP-Vollständigkeiteingeführt wurde [COO71]. Cook’s Beweis basiert dabei auf einer Reduktion vom Cliquenpro-blem.

2.6 Erdos Diskrepanzprobleme

Erdos Diskrepanz Vermutung

Eine ±1-Sequenz ist eine Sequenz, die nur die Zahlen 1 und −1 enthält, wobei beide Zahlen inder Sequenz gleich oft vorkommen.

Gegen 1932 hat der Mathematiker Paul Erdos die folgende Vermutung formuliert. Für eine unend-liche ±1-Sequenz 〈x1, x2, ...〉 und ein beliebiges C ∈ N existieren k, d ∈ N, so dass∣∣∣∣∣

k∑i=1

xi·d

∣∣∣∣∣ > C .

FürC = 2 haben Boris Konev and Alexei Lisitsa diese Vermutung bewiesen [KON14]. Sie zeigtenzunächst durch Kodierung des Problems mit SAT-Formeln und unter Verwendung der aktuellstenSAT-Solver das eine ±1-Sequenz mit der Diskrepanz 2 der Länge 1160 existiert. Dann bewiesensie: jede Sequenz der Länge 1161 hat mindestens eine Diskrepanz von 3.

17

Page 18: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Erdos Diskrepanzproblem

Nun lässt sich ein Entscheidungsproblem formulieren, dass fragt: Existiert eine endliche ±1-Sequenz 〈x1, x2, ..., xn〉 und ein 1 ≤ d ≤ n,m ≤ n/d, so dass∣∣∣∣∣∣

k/d∑i=1

xi·d

∣∣∣∣∣∣ ≤ 3 . (2.1)

18

Page 19: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 3

Aussagenlogik und SAT-Solving

3.1 Aussagenlogik

Bibliografische Hinweise Dieser Abschnitt basiert auf dem Buch Das ErfüllbarkeitsproblemSAT von Uwe Schöning und Jacobo Torán [SCH12] und dem Kapitel Aussagenlogik aus Komple-xitätstheorie und Kryptologie von Jörg Rothe [ROT08].

Historisch beginnt die Geschichte der Aussagenlogik bei Aristoteles, der bereits 384 vor der Zeit-rechnung aussagenlogische Grundsätze formulierte. Er sagte unter anderem wörtlich „Ein Satzist nun eine Aussage, welche etwas von einem Anderen bejaht oder verneint.“ Heute wird dieAussagenlogik als ein Teilgebiet der formalen Logik betrachtet.

Zunächst wird die Syntax der Aussagenlogik näher beleuchtet.

Definition 3.1 (Formel)Gegeben sei eine unendlich große, aber abzählbare Menge elementarer Aussagen V =

{x1, x2, x3, ...}, die auch als Aussagenvariablen oder Variablen bezeichnet werden. Die Mengeder aussagenlogischen Formeln FAL wird nun induktiv definiert:

• Die Konstanten 0 und 1 sind in FAL enthalten.

• Jede Variable aus V ist in FAL enthalten.

• Sind ϕ und ψ in FAL enthalten, dann sind auch ϕ, (ϕ ∧ ψ) und (ϕ ∨ ψ) in FAL enthalten.

Dabei werden folgende Bezeichnungen verwendet:

• ϕ heißt Negation.

• (ϕ ∧ ψ) heißt Konjunktion.

• (ϕ ∨ ψ) heißt Disjunktion.

• Ist ϕ eine Variable, dann kann sowohl ϕ als auch ϕ als Literal bezeichnet werden.

• Var(ϕ) ist die Menge aller Variablen, die in der Formel ϕ vorkommen.

19

Page 20: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Nun die Semantik.

Definition 3.2 (Wahrheitswert, Belegung)Ein Wahrheitswert ist ein Element der Menge {0, 1}. Sei V eine Teilmenge von V , dann wird eineAbbildung α : V → {0, 1} als Belegung bezeichnet, die einigen Variablen einen Wahrheitswertzuweist. Wir schreiben

α = {x1 = a1, x2 = a2, · · · } , ai ∈ {0, 1} .

Sei α eine Belegung und ϕ eine Formel, dann ist α total für ϕ, wenn V ⊇ Var(ϕ).

Darüber hinaus werden nun einige weitere Schreibweisen eingeführt, die sich im weiteren Verlaufder Arbeit als nützlich erweisen werden. Wir sagen, dem Literal u liegt die Variable x zugrunde,wenn gilt u = x oder u = x. Manchmal ist es praktisch wenn man anstatt eine Variable x miteinem Wahrheitswert a zu belegen, ein Literal u mit einem solchen belegt. Es gilt, wenn u = x,dann sind die Zuweisungen x = a und u = a gleichbedeutend und wenn u = x, dann sind dieZuweisungen x = a und u = 1− a gleichbedeutend.

Wenn in einer gegebenen Belegung der Wahrheitswert einer einzelnen Variable verändert oder beieiner nicht totalen Belegung zusätzlich belegt werden soll, dann ist die folgende Notation hilfreich.Gegeben sei eine Belegung

α = {x1 = a1, x2 = a2, ..., xi = ai, ...} .

Dann gilt für einen Wahrheitswert b,

α[xi = b] := {x1 = a1, x2 = a2, ..., xi = b, ...} .

Auch an dieser Stelle kann die Schreibweise verwendet werden, bei der anstatt einer Variableneinem Literal ein Wahrheitswert zugewiesen wird, wie oben beschrieben.

Definition 3.3 (Auswertung)Sei ϕ eine Formel und α eine Belegung mit Urbild V ⊆ V . Dann kann eine Formel ϕ durchα ausgewertet werden. Man sagt auch, dass α in ϕ eingesetzt wird. Die aus der Auswertungresultierende Formel ϕαwird gebildet, indem für jede Variable xi ∈ Var(ϕ)∪V alle Vorkommendieser in ϕ durch α(xi) ersetzt werden und folgende Vereinfachungen in ϕ durchgeführt werden.Sei ψ ∈ FAL, dann wird

• (ψ ∨ 0) oder (0 ∨ ψ) wird zu ψ,

• (ψ ∨ 1) oder (1 ∨ ψ) wird zu 1,

• (ψ ∧ 0) oder (0 ∧ ψ) wird zu 0,

• (ψ ∧ 1) oder (1 ∧ ψ) wird zu ψ,

• ¯ψ wird zu ψ und

• 0 wird zu 1 und 1 wird zu 0.

Bei dieser Definition muss man später nicht von unerfüllten Klauseln sprechen, sondern erfüllteKlauseln verschwinden und unerfüllte bleiben bestehen.

20

Page 21: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Definition 3.4 (Gültigkeit, Erfüllbarkeit)Sei eine Formel ϕ ∈ FAL. Wenn für eine Belegung α gilt ϕα = 1, dann sagen wir α erfüllt ϕ. DieFormel ϕ heißt erfüllbar, wenn eine Belegung α existiert, die ϕ erfüllt.

Ist eine Formel nicht erfüllbar, dann wird sie auch als unerfüllbar bezeichtnet. Aus der Definitionder Erfüllbarkeit ergibt sich nun unmittelbar das wichtigste Problem der Informatik, das Erfüllbar-keitsproblem.

Definition 3.5 (Erfüllbarkeitsproblem)Die Menge, die alle erfüllbaren Formeln enthält, wird SAT genannt. Die Frage, ob für eine gege-bene Formel ϕ gilt ϕ ∈ SAT, wird als Erfüllbarkeitsproblem bezeichnet.

Nun kommen wir zu einem sehr bedeutsamen Ergebnis der (theoretischen) Informatik. Im Jah-re 1971 bewies Stephen Cook das erste mal für ein natürliches Problem, dass es die Eigenschaftder NP-Vollständigkeit besitzt. Und zwar für das in diesem Abschnitt besprochene Erfüllbar-keitsproblem SAT. Für die Informatik ist dies ein historisches Ereignis, denn von nun an gab eseinen bekannten vollständigen Vertreter der KomplexitätsklasseNP und es konnten weitere Voll-ständigkeitsbeweise folgen, bei denen das Finden einer Polynomialzeitreduktion von SAT auf dasbetreffende Problem genügte. Bis zum heutigen Tage sind hunderte NP-vollständige Problemebekannt, die eine praktische Bedeutung haben.

Satz 3.1 (Cook, 1971 [COO71])Das Erfüllbarkeitsproblem ist NP-vollständig.

Für den Beweis dieser Aussage wird hier auf [COO71] oder [ROT08] verwiesen.

Definition 3.6 (Konjunktive Normalform)Die Menge der Formeln in konjunktiver Normalform (kurz: KNF) FKNF ⊂ FAL enthält alle For-meln, die das folgende Aussehen haben:

ϕ = ψ1 ∧ ψ2 ∧ · · · ∧ ψM

Die Teilformeln ψi werden als Klauseln bezeichnet und müssen wie folgt aussehen:

ψi = (ui,1 ∨ ui,2 ∨ · · · ∨ ui,ki)

Hierbei sind die ui,j Literale, also:

ui,j ∈ {x1, x2, · · · , xN , x1, x2, · · · , xN}

Die i-te Klausel hat die Länge |ψi| = ki. Für eine Konstante k befindet ϕ sich in k-konjunktiverNormalform (kurz: k-KNF), wenn für alle Klauseln ψ in ϕ gilt |ψ| ≤ k.

Definition 3.7 (Einheitsklausel)Eine Klausel der Länge 1 wird als Einheitsklausel bezeichnet.

Definition 3.8 (Pures Literal)Sei eine Literal u und eine Formel ϕ ∈ FKNF. Dann gilt, wenn die Klausel (u) in ϕ enthalten ist,dann ist u ein pures Literal für ϕ.

21

Page 22: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

3.2 SAT-Solver

Als SAT-Solver werden im allgemeinen Verfahren bezeichnet, die das k-SAT-Problem entschei-den. Sie erhalten also als Eingabe eine Formel in k-KNF und geben aus, ob diese erfüllbar ist.

Der denkbar einfachste SAT-Solver ist der Brute-Force-Algorithmus, der mit roher Gewalt jedeBelegung des gesamten Suchraums testet und stoppt, sobald eine Belegung die gegebene Formelerfüllt oder alle Belegungen getestet wurden. Allerdings beträgt die Größe des Suchraums 2N beieiner Formel mit N Variablen, weswegen wir hier schnell astronomische Laufzeiten erreichen.Ziel der verschiedenen Verfahren ist es daher, möglichst viele Belegungen als potentiell erfüllbareausschließen zu können und so den Suchraum zu verkleinern.

Ein einfaches Beispiel für einen SAT-Solver ist der folgende Backtracking-Algorithmus.

1 Algorithmus Backtracking(ϕ: Klauselmenge): bool2 if ϕ enthält leere Klausel then return 0 ;3 if ϕ ist leere Menge then return 1 ;4 wähle nach einer beliebigen Heuristik eine Variable x ∈ Var(ϕ) aus5 if Backtracking(ϕ{x = 0}) then return 1 ;6 return Backtracking(ϕ{x = 1})

Viele andere SAT-Solver basieren auf diesem Algorithmus.

3.3 DPLL

Der DPLL-Algorithmus ist ein SAT-Solver, der auf dem Backtracking-Algorithmus basiert. Erwurde benannt nach ihren Erfindern Davis, Putnam, Logeman und Loveland (Davis, Putnam, 1960[DP60] und Davis, Logeman, Loveland, 1962 [DPLL62]). Es ist ein deterministischer und voll-ständiger SAT-Solver, der wie folgt vorgeht.

1 Algorithmus DPLL(F : Klauselmenge): bool2 if F enthält leere Klausel then return 0 ;3 if F ist leere Menge then return 1 ;4 if F enthält Einheitsklausel {u} then return DPLL(F{u = 1}) ;5 if F enthält pures Literal u then return DPLL(F{u = 1}) ;6 x← H(ϕ) , wobei H eine Auswahlheuristik ist7 if DPLL(F{x = a}) then return 1 ;8 return DPLL(F{x = 1− a})

Wie bereits zu sehen ist, hängt der DPLL-Algorithmus nicht nur von der Eingabe der k-KNF-Formel ab, sondern auch von einer Heuristik H : Fk−KNF → V , die eine Variable auswählt, undvon einem Wahrheitswert a, der zuerst getestet wird.

In Zeile 4 des Algorithmus wird eine sogenannte Einheitsresolution (im Englischen: Unit Propa-gation) durchgeführt. Wenn in einer Formel ϕ in k-KNF eine Einheitsklausel (eine Klausel derLänge 1; im Englischen: Unit Clause) ψ = (u) existiert, dann ist u erfüllt oder ϕ ist unerfüllbar.Der DPLL-Algorithmus kann also den Wahrheitswert für die u zugrunde liegende Variable festle-gen und ψ und alle anderen Klauseln, die u enthalten, aus ϕ entfernen, ohne an der Erfüllbarkeit

22

Page 23: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

x1

x2

x3 x3

x4x4

x5

x6

ϕ erfüllbar(alle Klauseln entfernt)

Konflikt(leere Klausel gefunden)

ϕ{x1 = 1}

ϕ{x2 = 1}

ϕ{x3 = 1}

ϕ{x4 = 1} ϕ{x4 = 0}

ϕ{x3 = 0}

ϕ{x2 = 0} ϕ{x3 = 1}

ϕ{x4 = 1} ϕ{x4 = 0}

ϕ{x5 = 1} ϕ{x5 = 1}

ϕ{x6 = 1} ϕ{x6 = 0}

ϕ{x3 = 0}

Abbildung 3.1: DPLL-Algorithmus am Beispiel der im Anhang befindlichen aussagenlogischenFormel in 3-KNF mit 12 Variablen, die genau eine erfüllende Belegung besitzt. Der Algorithmusstartet hier im Wurzelknoten des Baumes und traversiert mittels Tiefensuche von links nach rechts.Ein Pfad endet, sobald ein Konflikt auftritt, d. h. wenn eine leere Klausel auftritt. Der Algorithmusterminiert in dem grün markierten Knoten.

etwas zu verändern. Mit anderen Worten: ϕ und ϕ{u = 1} sind erfüllbarkeitsäquivalent, wenn inϕ die Klausel (u) existiert.

Gegenüber dem Backtracking-Algorithmus ist hier noch eine weitere Regel hinzugekommen. InZeile 5 des DPLL-Algorithmus findet die sogenannte Pure-Literal-Rule Anwendung. Wenn ineiner k-KNF Formel ϕ ein Literal u vorkommt, aber dessen komplementäres Literal u nicht inϕ vorkommt, dann wird u als pures Literal bezeichnet. In so einem Fall haben wir wieder dieSituation, dass u erfüllt oder ϕ unerfüllbar ist. Und auch hier können wieder alle Klauseln, dieu enthalten aus ϕ entfernt werden, ohne die Erfüllbarkeit anzutasten. Kurz gesagt: Ist u in ϕ einpures Literal, dann sind ϕ und ϕ{u = 1} erfüllbarkeitsäquivalent.

In Abbildung 3.1 wird die Funktionsweise des DPLL-Algorithmus beispielhaft illustriert. Nunwird auch klar, wo der Vorteil gegenüber dem Brute-Force-Ansatz liegt. Für eine Formel mit NVariablen wird ein Suchbaum erzeugt, dessen Knoten und Kanten für die Variablenauswahl unddie Variablenbelegung stehen. Daher hat der binäre Baum eine maximale Tiefe von N und kannfolglich nicht mehr als 2N Knoten besitzten. Das Beispiel macht deutlich, dass auf einem Pfad einKonflikt entstehen kann und der Pfad nicht weiter verfolgt wird, bevor die maximale Tiefe erreichtwurde. Alle Variablenbelegungen, die auf diesem Pfad noch folgen würden, werden nicht mehr inBetracht gezogen und der Suchraum wird so verkleinert.

Um die nun folgenden DPLL-Heuristiken möglich kompakt und dabei aber auch präzise zu be-schreiben, ist es sinnvoll zunächst die Werte f (i)ϕ (u) und fϕ(u) zu definieren. Für eine k-KNFFormel ϕ und ein Literal u gibt f (i)ϕ (u) die Anzahl der Vorkommen von u in Klauseln von ϕ derLänge i an. Die Anzahl der Vorkommen von u in ϕ ist durch fϕ(u) =

∑ki=2 f

(i)ϕ (u) bestimmt.

23

Page 24: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Greedy DPLL-Heuristiken

DLIS, Dynamic Largest Individual Sum. Es wird die dem Literal arg maxu f(u) zugrunde-liegende Variable x ausgewählt und zuerst ϕ{x = 1} durchgeführt. Also

HDLIS(ϕ) = arg maxx

(max(fϕ(x), fϕ(x))) , aDLIS = 1 .

DLCS, Dynamic Largest Clause Sum. Es wird eine Variable durch

HDLCS(ϕ) = arg maxx

fϕ(x) + fϕ(x)

ausgewählt. Der zuerst angewendete Wahrheitswert ist durch

aDLCS(ϕ) =

{1 wenn fϕ(x) ≥ fϕ(x)

0 sonst

gegeben. Die Variante dieser Heuristik, bei der die zuerste angewendete Belegung zufällig gewähltwird, nennt sich RDLCS.

MOM, Maximum Occurence in Minimal Size Clauses. Auswahl der Variable durch

H(p)MOM(ϕ) = arg max

xp · (fϕ,l(x) + fϕ,l(x)) + fϕ,l(x) · fϕ,l(x) .

Wobei l die Länge der kleinsten, in ϕ vorkommenden, Klausel ist und p ein Parameter der Heuris-tik, der hinreichend groß gewählt werden muss, so dass stets gilt

p · (fϕ,l(x) + fϕ,l(x)) ≥ fϕ,l(x) · fϕ,l(x) .

Das führt dazu, dass die Variable, die in den kleinsten Klauseln am häufigsten vorkommt ausge-wählt wird. Gibt es mehrere Kandidaten, dann wird diejenige genommen, deren nichtnegierte undnegierte Literale möglichst gleich oft vorkommen.

Böhms-Heuristik. Für Variable x wird der Vektor J(x) = (J1(x), J2(x), · · · , Jk(x)) durch

Ji(x) = p1 ·max(fϕ,i(x), fϕ,i(x)) + p2 ·min(fϕ,i(x), fϕ,i(x))

definiert. Die Parameter p1 und p2 können frei gewählt werden. Es ergibt sich nun

H(p1,p2)Böhm (ϕ) = arg max

xJ(x) ,

wobei der maximale Wert gemäß der lexikographischen Sortierung von J(x) bestimmt wird.Bohms Heuristik wählt Variablen so, dass viele kleine Klauseln gelöscht werden können undgleichzeitig möglichst viele kleine Klauseln weiter verkleinert werden, um den Effekt der Ein-heitsresolution zu verstärken.

24

Page 25: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

3.4 Stochastic Local Search

Das Grundprinzip der lokalen Suche wird bei vielen kombinatorischen Problemen angewendet,nicht nur von SAT-Solvern. Es geht wie folgt:

1. Starte mit irgendeinem Lösungskandiaten für das Problem.

2. Ausgehend davon, dass der Kandidat keine optimale Lösung ist, führe lokale Verbesserun-gen an ihm durch.

Es gibt viele verschiedene Möglichkeiten solche Startkandidaten zu wählen, eine ist die randomi-sierte Auswahl. Dann wird von stochastischer lokaler Suche (Englisch: Stochastic Local Search)gesprochen. SLS wird schon lange gerade bei schweren kombinatorischen Optimierungsroble-men eingesetzt. Ein bekanntes Beispiel ist der Lin-Kerninghan-Algorithmus für das Problem desHandlungsreisenden aus dem Jahre 1973.

Obwohl Erfüllbarkeitsprobleme keine Optimierungsprobleme, sondern Entscheidungsproblemesind, lässt sich auch hier der SLS-Ansatz nutzen. Selman u.a. hat 1992 hierzu einen Algorithmusmit dem Namen GSAT und dessen Analyse vorgestellt [SEL92]. Dabei wird SLS wie folgt in SAT-Welt übertragen: Der Lösungskandidat, mit dem gestartet wird, ist eine Variablenbelegung für einegegebene Formel mit Wahrheitswerten, bei der eine lokale Optimierung durchgeführt wird, indemnach bestimmten Kriterien eine Variable der Formel ausgewählt und dessen Belegung verändertwird. Dies wird solange getan, bis eine erfüllende Belegung gefunden wurde oder bis solange ge-sucht wurde, dass die Wahrscheinlichkeit noch eine erfüllende Belegung zu finden, sehr gering ist.Dann wird davon ausgegangen, dass die Formel unerfüllbar ist. Genauer:

1 Algorithmus GSAT(ϕ: Klauselmenge; t1, t2: N): bool2 for i := 1, 2, ..., t1 do3 Wähle eine zufällige und totale Belegung α4 for j := 1, 2, ..., t2 do5 if ϕα = 1 then return 1 ;6 Wähle eine Variable x ∈ Var(ϕ) nach einer Heuristik7 α := α[x = 1− xα]

8 return 0

Sofern die Formel ϕ erfüllbar ist, ist für die Wahrscheinlichkeit pTP, dass GSAT eine erfüllendeBelegung findet, zwar positiv, aber das gilt ebenso für die Wahrscheinlichkeit PFN, dass keinegefunden wird, obwohl sie existiert. Auf der anderen Seite gilt, wenn ϕ unerfüllbar ist, dann liefertGSAT immer ein korrektes Ergebnis, also pFP = 0 und pTN = 1. Denn wenn ϕ keine erfüllendeBelegung besitzt, dann wird die Bedingung in Zeile 5 niemals erfüllt sein und folglich liefert derAlgorithmus niemals den Wert 1 (die Formel ist erfüllbar). Wir haben es hier also mit einem MonteCarlo Algorithmus zu tun, der einen einseitigen Fehler hat. Oder anders gesagt, es handelt sich umeinen unvollständigen SAT-Solver.

Die Wahrscheinlichkeiten pTP = 1 − pFN hängen von den gewählten Zeitparametern p1, p2 undvon der verwendeten Heuristik ab. Alternativ kann der Algorithmus auch so modifiziert werden,dass nicht die Laufzeit fest ist, sondern die Fehlerwahrscheinlichkeit. Dann hinge die Laufzeit desAlgorithmus von einer als akzeptabel deklarierten Fehlerwahrscheinlichkeit ab.

25

Page 26: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Mögliche Heuristiken zur Auswahl der Variable können die folgenden sein.

• Wähle eine Variable, so dass beim Negieren ihrer Belegung die Anzahl der unerfüllten Klau-seln in ϕ minimal ist.

• Minimiere die Anzahl der Klauseln, die durch lokale Änderung der der Belegung unerfülltwerden.

• Weise den Literalen einer Klausel eine Wahrscheinlichkeit mittels einer Heuristik zu (z.B.eine der beiden obigen) und wähle zufällig auf Basis der Wahrscheinlichkeitsverteilung.

Die beiden ersten Heuristiken verdeutlichen die grundsätzliche Strategie, sind aber in der Praxisungeeignet, da sie schnell in lokale Minima geraten. Die dritte bevorzugt zwar bestimmte Lite-rale, aber trifft die Wahl immer noch zufällig und hat daher eine Chance aus lokalen Minima zuentkommen.

3.5 Random Walk von Schöning

Der Random-Walk-Algorithmus von Schöning wurde veröffentlicht von Uwe Schöning im Jahr1999 [SCH99] und ist eine Umsetzung des im vorherigen Abschnitt beschriebenen prinzipiellenGSAT Algorithmus, der eine lokale Suchstrategie verwendet. Schönings Algorithmus nutzt dabeidie folgende Heuristik zur Auswahl der Variablen: Wähle eine durch die Belegung nicht erfüllteKlausel, aus dieser wähle zufällig ein Literal und verwende dessen zugrundeliegende Variable.

1 Algorithmus Schoening(ϕ: Klauselmenge): bool2 N := |Var(ϕ)|3 k := max{|C| | C ∈ ϕ}4 t := (2− 2/k)N

5 for i := 1, 2, ..., t do6 Wähle eine zufällige und totale Belegung α7 for j := 1, 2, ..., 3N do8 if ϕα = 1 then return 1 ;9 Wähle eine Klausel ψ ∈ ϕ mit ψα = 0

10 Wähle ein Literal u in ψ zufällig11 α := α[u = 1− uα]

12 return 0

Die Laufzeit des Algorithmus ergibt sich aus der Anzahl der Schleifendurchgänge (Zeile 5) undbeträgt O∗((2 − 2/k)N ), wobei der polynomielle Faktor, der sich aus der lokalen Suche unddem Testen der Variablenbelegung ergibt, hier nicht weiter berücksichtigt wurde. Nimmt man nunkonkrete Werte für k an, so erhalten wir die in der folgenden Tabelle angegebenen Laufzeiten.

k 3 4 5 6 7 8 ... ∞(2− 2/k)N 1,333N 1,5N 1,6N 1,667N 1,714N 1,75N ... 2N

Tabelle 3.1: Theoretische Laufzeiten für Schönings k-SAT-Algorithmus in Abhängigkeit von kund der Variablenanzahl N der Eingabeformel.

26

Page 27: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Analyse mittels Markow-Ketten

Nun wird die lokale Suchstrategie in Schönings SAT-Algorithmus mit Hilfe vom Markowkettenanalysiert. Zunächst folgt daher eine Definition des Begriffs der Markowkette, die auf [HAG02]basiert.

Definition 3.9 (Markowkette)Ein diskreter stochastischer Prozess (Xt)t∈N0 mit Werten aus dem endlichen Zustandsraum S =

{s1, s2, ..., sn} für alle Xt, heißt Markowkette mit Übergangsmatrix A, genau dann wenn für allet ∈ N0 und s0, s1, ..., st, st+1 ∈ S mit

P (Xt = st, Xt−1 = st−1, ..., X0 = s0) 6= 0 und

die folgenden beiden Aussagen gelten:

1. P (Xt+1 = st+1 | Xt = st, Xt−1 = st−1, ..., X0 = s0) = P (Xt+1 = st+1 | Xt = st) und

2. ∀r, s ∈ S : P (Xt) 6= 0⇒ P (Xt+1 = r | Xt = s) hängt nicht von t ab.

Eine stochastische Matrix P = (pi,j)ni,j=1 mit P (Xt+1 = j | Xt = i) = pi,j wird als Übergangs-

matrix der Markowkette bezeichnet.

Das Ziel der Analyse ist es, die Wahrscheinlichkeit q = q(N) zu bestimmen, mit der während derlokalen Suche in Schönings Algorithmus (vgl. obigen Algorithmus Zeile 7 bis 11) eine erfüllendeBelegung für die Eingabeformel gefunden wird. Die Anzahl t der notwendigen Wiederholungen,damit die Wahrscheinlichkeit, eine erfüllende Belegung zu finden, nahe bei 1 liegt, kann danndurch O(1/q(N)) bestimmt werden.

Da die folgende Analyse eine obere Abschätzung ist, nehmen wir an, dass nur eine erfüllendeBelegung existiert. Sei ϕ eine Formel mit N Variablen und α∗ die erfüllende Belegung für ϕ.Nun sei weiterhin α eine zufällig gewählte Belegung für ϕ und die Zufallsvariable H gebe dieHamming-Distanz zwischen α und α∗ an. Da wir die lokale Suche mit einer zufällig gewähltenBelegung starten, beträgt die erwartete Hamming-Distanz zu Beginn N/2. H ist binominalverteiltund es gilt

Pr(H = j) =

(N

j

)2−N .

Nun wissen wir, dass in jeder Klausel von ϕ mindestens ein Literal existiert, dass durch α erfülltwird. Die Wahrscheinlichkeit das der Algorithmus zufällig dieses Literal auswählt, und somitdurch Änderung der Belegung der zugrundeliegenden Variable die Hammbing-Distanz H um 1verringert, beträgt 1/k. Wir können also festhalten, dass im erwarteten Fall H = N/2 zumindestN/2 Suchschritte notwendig sind, um die erfüllende Belegung zu finden.

Wenn wir nun die lokale Suche von Schöning als Markowkette modellieren, erhalten wir den Zu-standsgraph in Abbildung 3.2. Der Zustand S ist der Startzustand und die übrigen Zustände stehenfür die entsprechende Hamming-Distanz zwischen der aktuellen Belegung α und der erfüllendenα∗. Die Kantenbeschriftungen sind die Zustandsübergangs-Wahrscheinlichkeiten. Die Frage istnun, wie groß ist die Wahscheinlichkeit nach s Schritten den Zustand 0 zu erreichen.

27

Page 28: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

S

jj − 1 j + 1· · ·210

erfüllendeBelegung

· · · n

(n0

)2−n(n1

)2−n(n2

)2−n

(nj−1)2−n

(nj

)2−n

(nj+1

)2−n

(nn

)2−n

11k

k−1k

1k

k−1k

1k

k−1k

1k

k−1k

1k

k−1k

1k

k−1k

1k

k−1k

1k

Abbildung 3.2: Schönings lokale Suche modelliert als Markowkette. Dargestellt durch einen Zu-standsautomaten mit den Übergangswahrscheinlichkeiten als Kantenbeschriftung. Mit dem Zu-stand S als Startzustand und dem Zustand 0, in dem die erfüllende Belegung gefunden wird.

Aus dem Zustandsautomaten ergibt sich nun die folgende Übergangsmatrix mit den Zustandsübergangs-Wahrscheinlichkeiten.

P =

0(n0

)2−n

(n1

)2−n

(n2

)2−n

(n3

)2−n

(n4

)2−n ...

(nn

)2−n

0 1 0 ... 0

0 1/k 0 (k − 1)/k 0 0 0 0

0 0 1/k 0 (k − 1)/k 0 0 0

0 0 0 1/k 0 (k − 1)/k 0 0...

......

......

......

...0 0 0 0 0 1/k 0 (k − 1)/k

0 0 0 0 0 0 1/k 0

Im folgenden bezeichnet der Ausdruck w[i] den Wert wi eines Vektors w = (w1, w2, ..., wk). Ge-mäß des Markowketten-Modells beträgt die Wahrscheinlichkeit nach t Zeitschritten den Zustandz zu erreichen

Pr(Xs = z) = (~v Ps)[z]

Demzufolge ist die Wahrscheinlichkeit, dass bei einer lokalen Suche, wie sie im AlgorithmusSchoening durchgeführt wird, die erfüllende Belegung, also den Zusatnd 0, nach 3N Zeit-schritten zu erreichen, gleich

Pr(X3N = 0) = (~v P3N )[0]

In seiner Analyse stellt Schöning für diese Wahrscheinlichkeit eine obere Abschätzung mit Hilfedes sogenannten „Ballot theorems“ [FEL68] an. Um zu erfahren, wie nahe diese obere Abschät-zung an die Werte aus dem Markowketten-Modell heranreicht, wurde die Markowkette für dieWerte N = 30, 90, 270, 810 simuliert und dessen Ergebnisse in den folgenden Diagrammen inAbbildung 3.3 dargestellt. Es ist zu beobachten, dass die Wahrscheinlichkeit schon nach wenigerals 3N Schritten (gekennzeichnet durch die gestrichelte Linie) den fast höchsten Wert erreicht.Somit könnte die Abschätzung von Schöning möglicherweise noch verbessert werden.

28

Page 29: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

0 30 60 90 120 150 180s0.0

0.5

1.0

1.5

Pr(X

s=

0)×10−4

N = 30

0 90 180 270 360 450 540s0

1

2

3

4

5

6

Pr(X

s=

0)

×10−12

N = 90

0 270 540 810 1080 1350 1620s0.0

0.5

1.0

1.5

2.0

Pr(X

s=

0)

×10−34

N = 270

0 810 1620 2430 3240 4050 4860s0

1

2

3

4

5

6

Pr(X

s=

0)

×10−102

N = 810

Abbildung 3.3: Die Wahrscheinlichkeit, dass Schönings lokale Suche die erfüllende Belegungfindet, in Abhängigkeit der Schrittanzahl s und der Variablenanzahl N im Fall k = 3.

Die obere Abschätzung der Laufzeit von Schönings Algorithmus beruht auf der Annahme, dass dieEingabeformel genau eine erfüllenden Belegung besitzt und dass in jeder Klausel der Formel ge-nau ein Literal durch diese Belegung erfüllt ist. Daher beträgt die Wahrscheinlichkeit, dass wir beieinem lokalen Suchschritt in einer Klausel das richtige Literal auswählen, gerade 1/3. Allerdingsmüssen wir dann auch beachten, dass in einer solchen Formel ein Ungleichgewicht der positivenund negativen Literale herrscht. Gehen wir einmal davon aus, dass (1)N unsere erfüllende Bele-gung der N Variablen ist, dann stehen N positive und N negative Literale zur Verfügung. Besitztunsere Formel in 3-KNF M Klauseln, so benötigen wir M der positiven und 2M der negativenLiterale um die Klauseln zu befüllen. Eine solche Formel mag den Worst-Case für Schönings Al-gorithmus darstellen, aber für einen DPLL-Algorithmus mit einer entsprechenden Heuristik wirdsie kein großes Problem darstellen, da durch das Ungleichgewicht der Literale die Formel bei derResolution schnell verkleinert werden kann und somit Konflikte schneller auftreten, als wenn posi-tive und negative Literale aller Variablen gleich oft auftreten. Wir müssen also festhalten, dass eineFormel, die einen Worst-Case für Schönings lokalen Suchalgorithmus darstellt, nicht unbedingt imAllgemeinen schwer auf Erfüllbarkeit zu prüfen ist.

Ein weiterer Aspekt für die Frage, wie lange es dauert eine existierende erfüllende Belegung zufinden, ist die Abhängigkeit der Klauseln untereinander. Nehmen wir einmal an, eine Variable xkommt in zwei unterschiedlichen Klauseln c, d in einer Formel als positives in c und negativesin d vor und nehmen wir weiter an, dass c durch die aktuelle Belegung nicht erfüllt und d erfülltist, dann kann es passieren, wenn der Algorithmus in einem lokalen Suchschritt die Klausel causwählt und sich zufällig für das Literal x entscheidet, was zur Änderung von dessen Belegungführt. Wodurch dann die Klausel c erfüllt ist und die Klausel d ist es nicht mehr. Wir stellen alsofest, der nötige Aufwand des Algorithmus, eine erfüllende Belegung zu finden hängt auch von denAbhängigkeiten zwischen den Klauseln ab.

29

Page 30: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

3.6 Ein Verfahren basierend auf Message-Passing

Diese Methode ist motiviert durch das Ising-Modell aus der statistischen Physik und gehört in dieKlasse der Message Passing Algorithmen. Das nun folgende Verfahren ist randomisiert und nichtvollständig. Die Suchstrategie nach einer erfüllenden Belegung läuft wie folgt ab:

• Eine Klausel fragt die in ihr enthaltenen Variablen, mit welcher Wahrscheinlichkeit sie eineBelegung annehmen, so dass die Klausel erfüllt wird.

• Je schlechter die Gesamtsituation, desto stärker fordert die Klausel von den Variablen ihreBelegung zu ändern.

• Wenn sich die Forderungen der Klauseln an die Variablen und die eventuelle Zustimmungder Variablen kaum noch verändern, dann wird die Verhandlung beendet und die Variablendem stärksten Trend entsprechend belegt.

• Falls die Belegung nicht erfüllend ist, wird eine neue Verhandlung gestartet.

In diesem Verfahren kommunizieren die Klauseln mit den Variablen, die in ihnen vorkommenund die Variablen mit den Klauseln in denen sie enthalten sind. Ein Graph, der die Kommuni-kationsteilnehmer und Kommunikationsverbindungen darstellt, ist ein bipartiter Graph mit zweiKantentypen. Es kann sein, dass die Verhandlungen nicht konvergieren.

3.7 Conflict Driven Clause Learning

Hierbei handelt es sich um einen deterministischen und vollständigen SAT-Algorithmus, der eineWeiterentwicklung des DPLL-Verfahrens darstellt.

1 Algorithmus CDCL(F : Klauselmenge): bool2 while Var(F) 6= ∅ do3 wähle eine Variable x und belege sie mit einem Wahrheitswert w (Entscheidung)4 führe Einheitsresolution F{x = w} durch5 berechne den Implikationsgraph G von F unter der Annahme, dass F erfüllbar6 if G enthält Konflikt then7 bestimme Konfliktklausel C und füge sie F hinzu8 mache geeignete Entscheidungen rückgängig, s.d. C eine Einheitsklausel ist

9 return 1

Im Implikationsgraph werden zunächst die Knoten zugefügt, die eine Zuweisung eines Wahrheits-wertes zu einer Variable darstellen. Weiterhin werden die Knoten eingefügt, die unter der An-nahme, dass die Formel erfüllbar ist, eine Implikation eines Wahrheitswertes zu einer Variablendarstellen. Die Implikationen werden durch Kanten mit den entsprechenden Zuweisungen verbun-den. Wenn zum Beispiel die Klausel (x1, x2) in einer Formel enthalten ist und x1 = 0 zugewiesenwird, dann erhalten wir die Implikation x2 = 1.

30

Page 31: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Wenn in einem Implikationsgraph ein Konflikt existiert, kann eine Konfliktklausel konstruiert wer-den. Man identifiziert die beiden Knoten, die einen Konflikt darstellen, und nimmt die Variablender Knoten, die mit einer der beiden Konfliktknoten direkt verbunden sind, in eine Klausel auf.Wenn die Variablen im entsprechenden Knoten den Wahrheitswert 1 erhalten haben, dann wird sienegiert.

3.8 Vorstellung von implementierten SAT-Solvern

EagleUP

Der SAT-Solver EagleUP wurde von Oliver Gableske u. a. an der Universität Ulm entwickelt und2011 veröffentlicht [GAB11]. Er kombiniert Paradigma Stochastic Local Search mit der Einheits-resolution und ist speziell für zufällige, erfüllbare 3-SAT-Formeln optimiert. Dieser Solver hatden dritten Platz bei der SAT Competition 2011 in der Kategorie „zufällige erfüllbare Formeln“erreicht. EagleUP besitzt keine Parallelverarbeitungfunktionalität und wurde in der Porgrammier-sprache C implementiert. Da er auf SLS basiert, ist er ein randomisierter, nicht vollständiger SAT-Solver.

adaptg2wsat

Dieser SAT-Solver wurde entwickelt von Wanxia Wei, Chu Min Li und Harry Zhang von der Uni-versity of New Brunswick beziehungsweise Université de Picardie Jules Verne und wurde im Jahr2007 zum ersten mal veröffentlicht [WEI07], aber später noch weiterentwickelt. Er kombiniertden Adaptive Noise und Look-Ahead Mechanismus für das Stochastic Local Search Paradigmaund ist daher ein randomisierter nicht vollständiger SAT-Solver. adaptg2wsat erzielte bei der SAT

Competition 2011 einen der vorderen Plätze in der Kategorie „zufällige erfüllbare Formeln“.

ppfolio

Bei ppfolio handelt es sich um einen sogenannten Parallel Portfolio Solver. Das heißt, er startetverscheidene SAT-Solver und lässt diese parallel laufen. Wenn einer von ihnen eine Lösung findet,dann werden auch die anderen terminiert. ppfolio wurde entwickelt von Olivier Roussel an derUniversität Artois und 2011 veröffentlicht [ROU11]. Dieser Portfolio Solver verwendet nachfol-gende SAT-Solver.

• cryptominisat (Mate Soos)

• lingeling/plingeling (Armin Biere)

• clasp (Martin Gebser, Benjamin Kaufmann, Torsten Schaub)

• TNM (Wanxia Wei, Chu Min Li)

• march_hi (Marijn Heule, Hans Van Maaren)

31

Page 32: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Er unterstützt Parallelverarbeitung mit beliebig vielen Prozessen, wobei zunächst jeder Solvereinen Prozessorkern zugewiesen bekommt. Wenn mehr als fünf Prozesse verwendet werden, be-kommt lingeling die übrigen Ressourcen zur Verfügung gestellt. ppfolio ist ein vollständiger SAT-Solver. Es gibt von diesem Solver verschiedene Versionen, die für verschiedene Arten von Formelnoptimiert sind. In dieser Arbeit wurde die Variante gewählt, die für zufällige Formeln angepasstist.

sattime

Sattime ist ein Stochastic Local Search SAT-Solver, der sich die Erfüllbarkeitshistorie der Klauselnzunutze macht, um zu entscheiden welche Variable bei der lokalen Suche als nächstes ausgewähltwird. sattime wurde von Chun Min Li u. a. an der Universität der Pikardie Jules Verne entwickeltund 2012 veröffentlicht [LI12]. Er hat aber bereits an der SAT Competition 2011 teilgenommenund den zweiten Platz in der Kategorie „zufällige erfüllbare Formeln“ gewonnen. Auch für diesenSolver gilt: Da es ein auf SLS basierender Solver ist, ist er randomisiert und nicht vollständig.

selector

Hier handelt es sich um einen Portfolio SOLVER, der zunächst eine umfangreiche Analyse derEingabeformel durchführt, um dann aus einem Portfolio von Solvern einen auszuwählen, der amehesten geeignet scheint, um die Erfüllbarkeit der Formel festzustellen. Er wurde entwickelt vonMeinolf Sellmann und verwendet die nachfolgenden SAT-Solver.

• adaptg2wsat2009, adaptg2wsat2009++ (Wanxia Wei, Chu Min Li, Harry Zhang)

• clasp (Martin Gebser, Benjamin Kaufmann, Torsten Schaub)

• cryptominisat (Mate Soos)

• glucose (Gilles Audemard, Laurent Simon)

• gnovelty+2, gnovelty+2-H (Duc-Nghia Pham, Charles Gretton)

• hybridGM3

• kcnfs04SAT07

• lingeling (Armin Biere)

• LySATc, LySATi (Youssef Hamadi, Saïd Jabbour, Lakhdar Saïs)

• march_hi, march_nn (Marijn Heule, Hans Van Maaren)

• minisat (Niklas Sorensson)

• mxc-sat09

• picosat, precosat (Armin Biere)

• SATenstein

32

Page 33: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

• TNM (Wanxia Wei, Chu Min Li)

• ubcsat

sparrow

Der SAT-Solver sparrow wurde von Andreas Balint u. a. an der Universität Ulm entwickelt undbasiert auf dem Stochastic Local Search Paradigma. Daher handelt es sich um einen randomisier-ten, nicht vollständigen Solver. Die in dieser Arbeit verwendete Version wurde 2011 veröffentlich[BAL11]. Er erreichte den ersten Platz bei der SAT Competition 2011 in der Kategorie „zufälligeerfüllbare Formeln“.

cirminisat

Bei diesem Solver handelt es sich um eine Weiterentwicklung des SAT-Solvers Minisat von NiklasEén und Niklas Sörensson, der auf dem Paradigma Conflict Driven Clause Learning und somitauch auf dem DPLL Algorithmus basiert. Er wurde entwickelt von Tomohiro Sonobe und MaryInaba an der Universität Tokio und 2012 veröffentlicht [SON12], hat aber bereits an der SAT

Competetion 2011 teilgenommen.

MPhaseSAT

Der SAT-Solver MPhaseSAT basiert auf Confilict Driven Clause Learning und somit ebenfalls aufdem DPLL Algorithmus. Desweiteren kommen Methoden wie Phase Selection, Boolean Cons-traint Propagation und Conflict Analysis zum Einsatz. Er wurde entwickelt von Jingchao Chenund 2011 veröffentlicht [CHE11]. Bei der SAT Competition hat es MPhaseSAT in vielen Katego-rien auf die vorderen Plätze geschafft. Es ist ein vollständiger Solver.

plingeling

Der SAT-Solver plingeling ist die parallelisierte Variante von lingeling. lingeling wurde entwickeltvon Armin Biere und ist ein Confilict Driven Clause Learning basierter vollständiger Solver. Indieser Arbeit wurde die 2011 veröffentlichte Variante eingesetzt [BIE11].

33

Page 34: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

34

Page 35: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 4

Konstruktion von SAT-Formeln

4.1 Reduktion von Graph-Färbbarkeit

Konstruktion 3-färbbarer Zufallsgraphen

Einen Zufallsgraphen, der die Eigenschaft der 3-Färbbarkeit besitzt, kann durch folgendes Vorge-hen konstruiert werden. Man erstellt drei gleich große Mengen von Knoten und färbt alle Knoteninnerhalb einer Menge mit der gleichen Farbe. Nun iteriert man durch alle Knotenpaarungen mitder Bedingung, dass die zwei Knoten nicht aus der gleichen Menge stammen. Mit einer Wahr-scheinlichkeit p wird eine Kante zwischen die beiden Knoten zugefügt. Der folgende Algorithmus3ColorableGraph präzisiert diese Konstruktionsmethode. Er konstruiert einen ungerichteten,3-färbbaren Zufallsgraphen G = (V,E) mit |V | = n Knoten und einer erwarteten Anzahl von

EW (|E|) = p ·(n

3· 2n

3+n

3· n

3

)=pn2

3

Kanten.

1 Algorithmus 3ColorableGraph(n: N, p: [0, 1]): Graph2 V := {v1,1, ..., v1,n/3} ∪ {v2,1, ..., v2,n/3} ∪ {v3,1, ..., v3,n/3}3 E := ∅4 forall the vi,s, vj,t ∈ V mit i 6= j und vi,s < vj,t do5 wähle r ∈ {0, 1} zufällig mit P (0) = 1− p und P (1) = p

6 if r = 1 then E := E ∪ {{vi,s, vj,t}};7 return (V,E)

Reduktion von 3-Färbbarkeit auf 3-SAT

Um das 3-Färbbarkeitsproblem für einen gegebenen Graphen G = (V,E) in das Erfüllbarkeits-problem für eine Formeln in 3-KNF zu überführen, beginnen wir mit folgender Überlegung. Fürjeden Knoten v ∈ V können wir Aussagen über die dessen Farbe formulieren.

• xv,1 := „v ist mit 1 gefärbt“

35

Page 36: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

• xv,2 := „v ist mit 2 gefärbt“

• xv,3 := „v ist mit 3 gefärbt“

Wir sagen G ist 3-färbbar genau dann, wenn für jeden Knoten v ∈ V mindestens eine der obigenAussagen wahr ist und folgendes gilt: Existiert eine Kante {u, v} ∈ E und es gilt xv,c für eineFarbe c ∈ {1, 2, 3}, dann gilt auch xu,c. Weiterhin gilt

xv,c ⇒ xu,c ⇔ xu,c ∨ xu,c .

Die obeigen Aussagen lassen sich einfach als aussagenlogische Klauseln formulieren und zu einerFormel in 3-KNF zusammensetzen. Dies tut der folgende Algorithmus ColoringTo3SAT. Erliefert eine Formel in 3-KNF mit N = 3 · |V | Variablen und M = |V | + 3 · |E| Klauseln, wobei|V | Klauseln die Länge 3 und 3 · |E| die Länge 2 haben.

1 function ColoringTo3SAT((V,E): Graph): Klauselmenge2 ϕ := ∅3 forall the v ∈ V do4 ϕ := ϕ ∪ {(xv,1 ∨ xv,2 ∨ xv,3)}5 forall the {u, v} ∈ E do6 ϕ := ϕ ∪ {(xv,1 ∨ xv,1)}7 ϕ := ϕ ∪ {(xv,2 ∨ xv,2)}8 ϕ := ϕ ∪ {(xv,3 ∨ xv,3)}9 return ϕ

Zufällige erfüllbare 3-SAT-Formeln durch 3-Färbbarkeit

Diese beiden Methoden lassen sich nun kombinieren, um (teilweise) zufällige, erfüllbare 3-SAT

Formeln zu generieren.

1 function ColoringCNF(n: N, p: [0, 1]): Klauselmenge2 G = (V,E) := 3ColorableGraph (n, p)

3 ϕ := ColoringTo3SAT (G)

4 return ϕ

Wir erhalten eine Formel in 3-KNF mit

N = 3 · |V | = 3n

Variablen und einer erwarteten Anzahl von Klauseln

M = |V |+ 3 · |E| = n+ 3 · EW (|E|)⇔ E(M) = n+ pn2 .

36

Page 37: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

4.2 Reduktion von Hypergraph-Färbbarkeit

Konstruktion zufälliger, 3-färbbarer Hypergraphen

Ähnlich wie einen 3-färbbaren Zufallsgraph genieren wir auch einen 3-färbbaren, zufälligen und 3-uniformen Hypergraph. Zunächst erzeugen wir nKanten und färben diese mit drei Farben beliebig,aber so, dass alle drei Farben gleich oft vorkommen (abgesehen vom Rest, wenn die Knotenanzahlnicht durch drei teilbar ist). Nun iterieren wir durch die

(n3

)möglichen Kanten: Falls die Knoten

nicht alle gleich gefärbt sind, existiert diese Kante mit einer Wahrscheinlichkeit von p.

1 Algorithmus 3ColorableHGraph(n: N, p: [0, 1]): Hypergraph2 V := {0, 1, ..., n− 1}3 E := ∅4 Färbung c : V → {0, 1, 2} mit c(v) = v mod 3

5 forall the i, j, k ∈ V mit i < j < k do6 if c(i) 6= c(j) ∨ c(i) 6= c(k) ∨ c(j) 6= c(k) then7 Wähle r ∈ {0, 1} zufällig mit P (r = 1) = p und P (r = 0) = 1− p8 if r = 1 then E := E ∪ {{i, j, k}};

9 return (V,G)

Der resultierende Hypergraph hat |V | = n Knoten und eine erwartete Anzahl

EW (|E|) = p ·((

n

3

)− 3

(n/3

3

))von Kanten.

Reduktion Hypergraph-Färbbarkeit auf 3-SAT

Um das 3-Färbbarkeitsproblem für Hypergraphen auf das 3-SAT-Probelm zu reduzieren gehen wirähnlich vor wie bei der Reduktion von 3-Färbbarkeit von Graphen in Abschnitt 7. Gegeben sei einHypergraph H = (V,E) mit E ⊆ {{u, v, w} | u, v, w ∈ V und u < v < w}. Für jeden Knotenin v ∈ V definieren wir die folgende Aussagen.

• xv,1 := „v ist mit 1 gefärbt“

• xv,2 := „v ist mit 2 gefärbt“

• xv,3 := „v ist mit 3 gefärbt“

Wenn von diesen Aussagen für jeden Knoten jeweils mindestens eine wahr ist und wenn für jedeKante {i, j, k} ∈ E alle folgenden Aussagen gelten.

• xi,0 ⇒ xj,0 ∨ xk,0• xi,1 ⇒ xj,1 ∨ xk,1• xi,2 ⇒ xj,2 ∨ xk,2

37

Page 38: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Genau dann istH mit drei Farben färbbar. Der Algorithmus HColoringTo3SAT überführt nachdiesem Prinzip den Hypergraph H in eine 3-SAT Formel, die genau dann erfüllbar ist, wenn H3-färbbar ist.

1 function HColoringTo3SAT((V,E): Hypergraph): Klauselmenge2 ϕ := ∅3 forall the v ∈ V do4 ϕ := ϕ ∪ {(xv,0 ∨ xv,1 ∨ xv,2)}5 forall the {i, j, k} ∈ E do6 ϕ := ϕ ∪ {(xi,0 ∨ xj,0 ∨ xk,0)}7 ϕ := ϕ ∪ {(xi,1 ∨ xj,1 ∨ xk,1)}8 ϕ := ϕ ∪ {(xi,2 ∨ xj,2 ∨ xk,2)}9 return ϕ

Die resultierende Formel in 3-KNF besitzt N = 3 · |V | Variablen und M = |V |+3 · |E| Klauseln.Das Verhältnis von Klauseln zu Variablen beträgt

M

N=

1

3+|E||V | .

Zufällige erfüllbare 3-SAT-Formeln durch Hypergraph-Färbbarkeit

Diese zwei Verfahren aus den letzten beiden Abschnitten können nun verwendet werden, um (teil-weise) zufällige, garantiert erfüllbare 3-SAT Formeln zu erzeugen.

1 function HColoringCNF(n: N, p: [0, 1]): Klauselmenge2 G = (V,E) := 3ColorableHGraph (n, p)

3 ϕ := HColoringTo3SAT (G)

4 return ϕ

Wir erhalten eine Formel in 3-KNF mit

N = 3 · |V | = 3n

Variablen und einer erwarteten Anzahl von Klauseln

EW (M) = |V |+ 3 · EW (|E|)

= n+ 3p ·((

n

3

)− 3

(n/3

3

)).

4.3 Reduktion von X3C

Wie bereits in Abschnitt 2.4 ausgeführt wurde, handelt es sich bei dem X3C um einen Spezialfalldes Problems der exakten Überdeckung oder wie es im Englischen genannt wird, Exact-Cover.Um randomisierte, erfüllbare Formeln auf Basis von X3C zu konstruieren, werden wir zunächstrandomisierte X3C-Instanzen generieren und davon ausgehend eine Reduktion auf SAT durchfüh-ren.

38

Page 39: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Zufällige positive X3C-Instanzen

Gegeben sei eine Grundmenge U = {1, 2, ...,m}, dann ist eine triviale, U überdeckende Tripel-menge durch S = {{1, 2, 3}, {4, 5, 6}, ..., {n−2, n−1, n}} gegeben. Wenn wir erstens nun nochTripels mit Werten, die zufällig und für jedes Tripel ohne zurücklegen aus U gewählt werden, zu Shinzufügen und zweitens die Menge U vor der Zerlegung zufällig permutieren, dann erhalten wireine nicht-triviale Tripelmenge S, die U überdeckt, mit zufälligem Charakter. Nach diesem Ansatzerzeugt der folgende Algorithmus zufällige X3C-Probleminstanzen, die durch n,m parametrisiertsind. Die Größe der resultierenden Tripelmenge ist dabei durch n bestimmt und die Größe derGrundmenge durch m.

1 Algorithmus X3CInstance(n, m: N): X3C-Instanz2 U := {1, 2, ...,m}3 S := ∅4 while U 6= ∅ do5 Wähle x, y, z ∈ U zufällig ohne zurücklegen6 S := S ∪ {(x, y, z)}7 k := n−m/38 Wähle S1, ..., Sk ∈ {(x, y, z) ∈ U3 | x < y < z} zufällig mit zurücklegen9 S := S ∪ {S1, ..., Sk}

10 return (U, S)

Reduktion von X3C auf k-SAT

1 function X3CToSAT(U : Grundmenge, S: Menge von 3-Tupeln über U): Klauselmenge2 ϕ := ∅3 forall the j ∈ {1, 2, ..., |U |} do

4 ϕ := ϕ ∪{( ∨

i mit j∈Si

xi

)}5 forall the j, k ∈ {1, 2, ..., |S|} mit j < k do

6 if Sj ∩ Sk 6= ∅ then7 ϕ := ϕ ∪ {(xj ∨ xk)}

8 return ϕ

Nun werden X3C-Probleminstanzen (U, S) auf SAT-Formeln in n-KNF reduziert, wobei n = |S|.Für jedes Tripel in Si ∈ S verwenden wir eine xi. Die Variable ist wahr, genau dann wenn daszugeordnete Tripel zur exakten Überdeckung gehört. Die beiden folgenden Aussagen sind genaudann erfüllt, wenn S′ ⊆ S eine exakte Überdeckung von U darstellt.

• Für jedes j ∈ U existiert ein Si ∈ S′ das j enthält.

• Für alle Sj , Sk ∈ S′ gilt Sj ∩ Sk = ∅.

Diese Aussagen können mit Hilfe der Variablen x1, ..., xn auch in Form von aussagenlogischen

39

Page 40: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Klauseln formuliert werden, was der Algorithmus X3CToSAT für einen gegebene X3C-Instanzumsetzt. Die resultierende Formel ϕ enthält N = |S| Variablen und für die Anzahl der Klauselngilt die obere Grenze M ≤ |U |+

(|S|2

).

Zufällige erfüllbare k-SAT-Formeln durch X3C

Mit Hilfe der beiden obigen Methoden können nun randomisierte Formeln in n-KNF erzeugtwerden.

1 function X3CCNF(n, m: N): Klauselmenge2 (U, S) := X3CInstance(n,m)

3 ϕ := X3CToSAT(U, S)

4 return ϕ

Um Formeln zu erzeugen, die in 3-KNF sind, können n-Klauseln wie folgt zerlegt werden. Seieine Klausel ψ = (u1 ∨ u2 ∨ ... ∨ uk), dann ist die folgende Aussage genau dann erfüllt, wenn ψerfüllt ist.

(u1 ∨ u2 ∨ w1) ∧( k−2∧i=1

(wi ∨ ui+2 ∨ wi+1))∧ (wn−1 ∨ uk−1 ∨ uk)

Die neuen Variablen w1, ..., wk−1 werden dabei in die Formel eingefügt. Mit dieser Vorgehens-weise können Klauseln in dieser Formel zerlegt werden, ohne dass sich an der Erfüllbarkeit derFormel etwas ändert.

4.4 Reduktion von Teilgraph-Isomorphie

Konstruktion zufälliger positiver TI-Instanzen

Nach dem folgenden randomisierten Prinzip kann eine positive Probleminstanz für das Teilgraph-Isomorphie-Problem generiert werden. Erzeuge einen Zufallsgraphen G, fertige unter Umbenen-nung der Knoten eine Kopie H von G an, füge H weitere Knoten und Kanten hinzu. Der nachfol-gende Algorithmus beschreibt das Verfahren genauer.

1 function TIInstance(n, m: N; p: [0, 1]): Klauselmenge2 G = (VG, EG) := Gn,p mit VG = {1, 2, ..., n}3 H = (VH , EH) := kopiere(G)

4 Knotenumbenennung(H)

5 VH := VH ∪ {n+ 1, n+ 2, ..., n+m}6 forall the s ∈ VH , t ∈ {n+ 1, n+ 2, ..., n+m} do7 if s 6= t then8 Wähle r ∈ {0, 1} zufällig mit P (0) = 1− p und P (1) = p

9 if r = 1 then EH := EH ∪ {{s, t}};

10 return (G,H)

40

Page 41: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Reduktion von TI auf k-SAT

Gegeben die GraphenG = (VG, EG) mit |VG| = nG undH = (VH , EH) mit |VH | = nH . Für allevi ∈ VG, wj ∈ VH sei eine aussagenlogische Variable xi,j , die genau dann mit dem Wahrheitswert1 belegt wird, wenn vi auf wj abgebildet wird.

G ist genau dann zu einem beliebigen Teilgraphen von H isomorph, wenn die nachfolgendenAussagen wahr sind.

• Für alle vi ∈ VG gilt∨nHj=1 xi,j . (So wird sichergestellt, dass jeder Knoten von G auf einen

Knoten von H abgebildet wird.)

• Für alle vi ∈ VG und alle j, k ∈ {1, 2, ..., nH} mit j < k gilt xi,j ∨ xi,k. (So ist garantiert,dass jeder Knoten aus G auf maximal einen Knoten aus H abgebildet wird.)

• Für alle i ∈ {1, 2, ..., nH} und alle j, k ∈ {1, 2, ..., nG} mit j < k gilt xj,i ∨ xk,i. (Dadurchwird garantiert, dass maximal ein Knoten aus G auf einen Knoten von H abgebildet wird.)

• Für alle i, j ∈ {1, 2, ..., nG} mit i < j und (vi, vj) ∈ EG und für alle k, l ∈ {1, 2, ..., nH}mit k < l und (wk, wl) /∈ EH gilt xi,k ∨ xj,l und xi,l ∨ xj,k. (So wird sichergestellt, dassjede Kante von G nur auf eine in H existierende Kante abgebildet werden kann.)

Aus diesen Aussagen können nun aussagenlogische Klauseln formuliert werden, die durch Kon-junktion verbunden sind. Der nachfolgende Algorithmus TIToSAT setzt das in die Tat um.

Die resultierende Formel ist in |VH |-KNF und hat N = |VH | · |VG| Variablen. Die Anzahl derKlauseln hängt von der Anzahl der Knoten und Kanten beider Graphen ab.

1 function TIToSAT((VG, EG), (VH , GH): Graph): Klauselmenge2 ϕ := ∅3 forall the vi ∈ VG do

4 ϕ := ϕ ∪{( |VH |∨

j=1

xi,j

)}5 forall the vi ∈ VG do6 forall the j, k ∈ {1, 2, ..., |VH |} mit j < k do7 ϕ := ϕ ∪ {(xi,j ∨ xi,k)}

8 forall the i ∈ {1, 2, ..., |VH |} do9 forall the j, k ∈ {1, 2, ..., |VG|} mit j < k do

10 ϕ := ϕ ∪ {(xj,i ∨ xk,i)}

11 forall the i, j ∈ {1, 2, ..., |VG|} mit i < j und (vi, vj) ∈ EG do12 forall the k, l ∈ {1, 2, ..., |VH |} mit k < l und (wk, wl) /∈ EH do13 ϕ := ϕ ∪ {(xi,k ∨ xj,l), (xi,l ∨ xj,k)}

14 return ϕ

41

Page 42: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Konstruktion von zufälligen k-SAT-Formeln durch TI

Der Algorithmus TICNF generiert Formeln in (n + m)-KNF mit n(n + m) Variablen. DurchZerlegung der Klauseln wie bereits in Abschnitt 4 beschrieben, lassen sich auch Formeln in 3-KNF erzeugen. Allerdings vergrößert sich so die Anzahl der Variablen.

1 function TICNF(n,m: N, p: [0, 1]): Klauselmenge2 (G,H) := TIInstance(n,m, p)

3 ϕ := TIToSAT(G,H)

4 return ϕ

4.5 Reduktion von EDP

Das hier beschriebene Verfahren basiert auf [KON14]. Die Reduktion des Diskrepanzproblemvon Erdos auf SAT wird mit Hilfe des Zustandsautomaten in Abbildung 4.1 durchgeführt. Fürjede ±1-Sequenz starten wir im Zustand 0. Die nächsten zwei Elemente der Sequenz bestimmenstets den Folgezustand.

Für jedes Element i einer±1-Sequenz der Länge k verwenden wir eine aussagenlogische Variablexi. Ist das Literal xi wahr, dann ist das Element i gleich 1, ansonsten −1.

Es gibt die Zeitschritte 1, 2, ..., k/2. Für jeden Zeitschritt j verwenden wir die Variablen yj undzj . Ist das Literal yj bzw. zj wahr, dann befinden wir uns zum Zeitpunkt j im Zustand −2 bzw. 2.

0−2 +2

E

+1−1,−1+1+1−1,−1+1 +1−1,−1+1

+1+1

−1−1

−1−1

+1+1

+1+1−1−1

Abbildung 4.1: Modellierung der Diskrepanz einer±1-Sequenz als Zustandsautomat. Der ZustandE bezeichnet dabei den Fehlerzustand. Wird dieser erreicht, hat die ±1-Sequenz zumindest eineDiskrepanz von 4.

Die folgenden aussagenlogischen Formeln gelten für jeden Zeitschritt j genau dann, wenn (2.1)gilt.

42

Page 43: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

• Zustand −2:

(x2j−1 ∧ x2j ∧ yj → yj+1 ∨ x2j−1 ∧ x2j ∧ yj → yj+1) ∧(x2j−1 ∧ x2j ∧ yj → yj+1) ∧

(x2j−1 ∧ x2j ∧ yj → e)

• Zustand 0:

(x2j−1 ∧ x2j ∧ yj ∧ zj → yj+1 ∨ x2j−1 ∧ x2j ∧ yj ∧ zj → yj+1) ∧(x2j−1 ∧ x2j ∧ yj ∧ zj → zj+1 ∨ x2j−1 ∧ x2j ∧ yj ∧ zj → zj+1) ∧

(x2j−1 ∧ x2j ∧ yj ∧ zj → zj+1) ∧(x2j−1 ∧ x2j ∧ yj ∧ zj → yj+1)

• Zustand +2:

(x2j−1 ∧ x2j ∧ zj → zj+1 ∨ x2j−1 ∧ x2j ∧ zj → zj+1) ∧(x2j−1 ∧ x2j ∧ zj → e) ∧

(x2j−1 ∧ x2j ∧ zj → zj+1)

• Zustand e:

e

Konstruktion von k-SAT-Formeln durch EDP

Die obigen Aussagen können leicht in Form von aussagenlogischen Klauseln formuliert werden.Der folgende Algorithmus beschreibt nun das Verfahren der Konstruktion einer Formel in KNF.

1 function EDPKNF(k: N): Klauselmenge2 ϕ := ∅3 for d = 1, 2, 3, ..., k do4 for j = 2, 4, 6, ..., k/d do5 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ yj/2+1 ∨ x(j−1)d ∨ xjd ∨ yj/2 ∨ yj+1 zu ϕ hinzu6 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ yj/2+1 zu ϕ hinzu7 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ e zu ϕ hinzu8 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ yj/2+1 ∨ x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ yj/2+1

zu ϕ hinzu9 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ zj/2+1 ∨ x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ zj/2+1

zu ϕ hinzu10 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ zj/2+1 zu ϕ hinzu11 füge x(j−1)d ∨ xjd ∨ yj/2 ∨ zj/2 ∨ yj/2+1 zu ϕ hinzu12 füge x(j−1)d ∨ xjd ∨ zj/2 ∨ zj/2+1 ∨ x(j−1)d ∨ xjd ∨ zj/2 ∨ zj/2+1 zu ϕ hinzu13 füge x(j−1)d ∨ xjd ∨ zj/2 ∨ e zu ϕ hinzu14 füge x(j−1)d ∨ xjd ∨ zj/2 ∨ zj/2+1 zu ϕ hinzu

15 return ϕ

43

Page 44: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

4.6 Vervielfältigung von Klauseln

Die Grundidee dieser Methode ist, dass ausgehend von einer festen 3-SAT-Formel durch semi-zufällige Vervielfältigung der Klauseln und Umbenennung der Variablen beliebig große 3-SAT-Formeln mit N Variablen und M Klauseln konstruiert werden. Auch das Verhältnis M/N istdabei variabel.

Der Konstruktionsalgorithmus erhält als Eingabe neben der festen Basisformel die Parametern,m ∈ N. Der Parameter n bestimmt, wie viele Kopien der Klauseln erstellt werden und m

gibt die Anzahl der Klauseln an, die in die resultierende 3-SAT-Formel übernommen werden. Esfolgt nun die exakte Beschreibung im Algorithmus Klauselkopien.

1 function Klauselkopien(F : Klauselmenge; n,m: N; e: bool): Klauselmenge2 n′ = |Var(F )|3 ϕ := ∅4 if e then5 forall the xi ∈ Var(F ) do6 füge Äquivalenzklauseln für Variablen x0n′+i, x1n′+i, ..., x(n−1)n′+i zu ϕ hinzu

7 forall the (ua, ub, uc) ∈ F do8 konstruiere eine (n× 3)-Matrix der Form

A =

u0n′+a u0n′+b u0n′+cu1n′+a u1n′+b u1n′+c

......

...u(n−1)n′+a u(n−1)n′+b u(n−1)n′+c

mit

u12j+i :=

{x12j+i, wenn ui = xi

x12j+i, wenn ui = xi

if Methode = random then9 führe auf jeder Spalte von A einen Shuffle durch

10 wähle zufällig m Zeilen und füge diese als Klauseln zu ϕ hinzu

11 if Methode = deterministisch then12 für j = 0, ...,m− 1 füge die Klausel (un′j+a, un′(j+1)+b, un′(j+2)+c) in ϕ ein

13 if Methode = detrand then14 wiederhole m mal: wähle zufällig eine Zahl j ∈ {0, 1, ..., n− 1} und füge die

Klausel (u12j+a, u12(j+1)+b, u12(j+2)+c) in ϕ ein

15 return ϕ

Äquivalenzklauseln

Als Äquivalenzklauseln bezeichnen wir eine Menge von Klauseln, die folgende Eigenschaft ha-ben: die Klauseln sind genau dann alle erfüllt, wenn die Variablen, die in ihnen vorkommen, allemit dem gleichen Wahrheitswert belegt sind. Sie dienen hier dazu, zu erzwingen, dass die konstru-

44

Page 45: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

ierte Formel nur eine erfüllende Belegung besitzt.

4.7 Zufällige Formeln in 3-KNF

1 function RandomCNF(N,M : N): Klauselmenge2 ϕ := ∅3 while |ϕ| < M do4 Wähle zufällig drei ganze Zahlen 1 ≤ i < j < k ≤ N5 Wähle zufällig drei ganze Zahlen 0 ≤ r, s, t ≤ 1

6 if r = 1 then u1 := xi else ui := xi7 if s = 1 then uj := xj else uj := xj8 if t = 1 then uk := xk else uk := xk9 ϕ := ϕ ∪ {(ui ∨ uj ∨ uk)}

10 return ϕ

Es konnte experimentell bestätigt werden, dass ein Schwellwert s ≈ 4,2 existiert, so dass dieWahrscheinlichkeit für eine erfüllbare Formel nahe bei 1 liegt, wenn M/N < s und die Wahr-scheinlichkeit für eine unerfüllbare Formel nahe bei 1 liegt, wenn M/N > s. Auch konnte durchExperimente gezeigt werden, dass dieser Phasenübergang am Schwellwert immer steiler verläuft,umso größer N ist (vergleiche [BIR02]). Diese Zusammenhänge konnten allerdings noch nichttheoretisch nachgewiesen werden.

45

Page 46: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

46

Page 47: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 5

Experimentelle Untersuchungen

5.1 Implementierung

Die Algorithmen zur Konstruktion von SAT-Formeln in KNF wurden als Kommandozeilenpro-gramme für Linux in der Programmiersprache C++ implementiert. Die generierte Formel wirdim DIMACS-Format auf die Standardausgabe STDOUT ausgegeben. So ist dem Anwender über-lassen, ob er die Formel in einer Datei speichert oder direkt mittels Piping an einen SAT-Solverweitergibt, der von der Standardeingabe STDIN liest.

Der SAT-Algorithmus von Schöning ist aus Geschwindigkeitsgründen ebenfalls in C++ imple-mentiert worden. Weiterhin wurde die OpenMP-Bibliothek verwendet um den Algorithmus zuparallelisieren. Das Arbeiten mit Zahlen, die größer als 64 Bit sind, wurde mit Hilfe der GMP-Bibliothek durchgeführt.

Die systematische Ausführung der Experimente wurde mit Python-Programmen durchgeführt, diegewonnenen Daten sind in einer SQLite3-Datenbank gesammelt worden. Bei der Auswertung derTestdaten kamen NumPy, SciPy und PyPlot zum Einsatz.

c Hier istc der Kommentarbereichp cnf 5 61 2 -5 02 5 4 0-1 3 -4 0-3 4 0-1 4 5 03 -4 5 0

Abbildung 5.1: Beispiel einer Formel mit 5 Variablen und 6 Klauseln in 3-KNF, die im DIMACS-Format dargestellt ist.

DIMACS ist ein Format für SAT Formel in KNF. Es besteht aus mehreren Zeilen, zunächst kommteine beliebige Anzahl von Kommentarzeilen, die mit dem Buchstaben „c“ beginnen müssen. Dann

47

Page 48: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

folgt eine Zeile „p cnf n m“, wobei „n“ durch die Anzahl der Variablen ersetzt werden muss und„m“ durch die Anzahl der Klauseln. Die Variablen der Formel müssen durchnummeriert sein.Denn jetzt kommt pro Klausel in der Formel eine weitere Zeile. Für jedes Literal wird dabei dieNummer der Variablen angegeben. Eine negierte Variable wird durch Angabe des negativen Zah-lenwertes kenntlich gemacht. Die Literale werden durch Leerzeichen getrennt und das Ende derKlausel durch eine „0“ gekennzeichnet. Nachfolgend ist ein Beispiel einer Formel mit 5 Variablenund 6 Klauseln im DIMACS-Format.

5.2 Testumgebung

Als Testrechner wurde ein Parallelrechner des Instituts für theoretische Informatik an der Univer-sität zu Lübeck verwendet. Er verfügt über 128 GB Arbeitsspeicher und acht AMD Opteron 6272Prozessoren, dessen Daten in der Tabelle 5.1 entnommen werden können.

Kerne 16Taktfrequenz 2,1 GHzCache L1 8 × 64 KB, 16 × 16 KBCache L2 8 × 2 MBCache L3 2 × 8 MB

Tabelle 5.1: Daten des AMD Opteron 6272 Prozessors.

In der Summe verfügt das Testsystem über 64 Prozessorkerne. Bei den Tests mit den parallelisier-ten SAT-Solvern sind daher auch stets 64 parallele Threads verwendet worden. Die Solver, auf diedas zutrifft, wurden dadruch kenntlich gemacht, dass sie die Zahl 64 am Ende des Namens tragen.

5.3 Auswertung der Testdaten

Worst-Case-Laufzeit Bei den meisten hier betrachteten Methoden zur randomisierten Kon-struktion von SAT-Formeln gibt es einen Parameter, von dem die Anzahl der Variablen in derFormel abhängig ist. Die übrigen Parameter bestimmen, wie schwer es ist die Formel auf Er-füllbarkeit zu prüfen. Um die Laufzeit der SAT-Solver in Abhängigkeit der Variablenanzahl zubestimmen, wurden stets die übrigen Parameter für eine feste Variablenanzahl so gewählt, dass diedurchschnittliche Laufzeit maximal war. Daher wird nachfolgend des öfteren von einer maximalenDurchschnitts-Laufzeit gesprochen.

Parameterbestimmung der Modellfunktionen Die asymptotischen Laufzeiten der SAT-Solverwurden mit Hilfe der Modellfunktion

f(N, a, b, c) = a+ b · 2cN

und der Methode der kleinsten Quadrate approximiert. Die Funktion ist zuvor logarithmiert wor-den.

48

Page 49: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

5.4 Vervielfältigung einer festen 3-SAT Formel

Die hier verwendeten SAT-Formeln wurden nach der Methode konstruiert wie im Abschnitt 4.6beschrieben. Es handelt sich um semizufällige Formeln, die durch Vervielfältigung der Klauselneiner festen 3-SAT Basisformel konstruiert werden. Die Größe der Formeln, also die Anzahl derVariablen und Klauseln, hängt dabei von den Parametern n,m ∈ N ab. Der Parameter n bestimmtdie Anzahl der Kopien, die von jeder Klausel der Basisformel erstellt werden und somit die Anzahlder Variablen N der resultierenden Formel. Der Parameter m bestimmt wieviele der n weiterver-arbeiteten Klauselkopien ausgewählt und in die resultierende Formel übernommen werden undbestimmt so über die Anzahl der Klauseln M in der resultierenden Formel. In diesem Experie-ment wird als Basisformel eine 3-KNF Formel mit 12 Variablen und 40 Klauseln verwendet, fürdie genau eine erfüllende Belegung existiert (siehe Anhang). In hier untersuchten Formeln beträgtdie Anzahl der Variablen also N = 12n und die Anzahl der Klauseln M = 40m.

Verwendete SAT-Formeln

Für n ∈ {3, 4, 5, 6, 7, 8} und verschiedene m werden Formeln jeweils mit den drei unterschiedli-chen Konstruktionsmethoden mit und ohne Äquivalenzklauseln erzeugt. Mit dem SAT-Algortihmusvon Schöning wurden die in der folgenden Tabelle angegebenen Meßpunkte getestet.

n m

3 1, 2, 3, ..., 30, 40, 50, ..., 100, 200, 500, 10004 1, 2, 3, ..., 30, 40, 50, ..., 100, 200, 500, 10005 1, 2, 3, ..., 30, 40, 50, ..., 100, 200, 500, 10006 1, 2, 3, ..., 12, 14, 16, ..., 20, 30, 40, ..., 100, 200, 500, 1000, 2000, 40007 5, 6, 7, 8, 9, 10, 15, 20, 30, 40, 50, 100, 200, 500, 1000, 2000, 40008 4, 5, 6, 7, 8, 9, 10, 11, 12, 30

Die Anzahl der generierten Formeln für jeden Meßpunkt n,m und für jede der sechs Variantendes Konstruktions-Algorithmus können der nun folgenden Tabelle entnommen werden.

n 3 4 5 6 7 8Formeln pro Methode und m 1000 500 100 100 50 25

Für die übrigen SAT-Solver wurde analog vergegangen. Allerdings sind Formeln mit bis zu 384Variablen verwendet worden.

Ergebnisse und Interpretation

Analyse der verschiedenen Konstruktionsvarianten

Deterministische Konstrunktionsvarianten sind ungeeignet, da sie bei bestimmten Parameterkom-bination Formeln mit extrem vielen erfüllenden Belegungen erzeugen. Auch bei Parameterwerten,wo dieser Effekt nicht aufgetreten ist, konnte nicht festgestellt werden, dass irgendein Vorteilgegenüber der rein randomisierten Varainte besteht. Daher wurde nachfolgendend nur noch dierandomisierte Variante verwendet.

49

Page 50: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

5 10 15 20 25 30m0.0

0.2

0.4

0.6

0.8

1.0

1.2

1.4

�ge

test

ete

Bel

egun

gen

×105

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(a) n = 3, N = 36

5 10 15 20 25 30m0.0

0.5

1.0

1.5

2.0

2.5

�ge

test

ete

Bel

egun

gen

×106

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(b) n = 4, N = 48

5 10 15 20 25 30m0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

4.5

�ge

test

ete

Bel

egun

gen

×107

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(c) n = 5, N = 60

5 10 15 20 25 30m0

1

2

3

4

5

6

�ge

test

ete

Bel

egun

gen

×108

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(d) n = 6, N = 72

5 10 15 20 25 30m0.0

0.2

0.4

0.6

0.8

1.0

�ge

test

ete

Bel

egun

gen

×1010

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(e) n = 7, N = 84

5 10 15 20 25 30m0.0

0.2

0.4

0.6

0.8

1.0

1.2

�ge

test

ete

Bel

egun

gen

×1011

mit Aquivalenzklauseln

ohne Aquivalenzklauseln

(f) n = 8, N = 96

Abbildung 5.2: Ergebnisse für Schönings SAT-Algorithmus bei Formeln, die durch Vervielfälti-gung erzeugt wurden. Der Parameter n ist fest und m ∈ [0, 1].

50

Page 51: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Charakteristik bei festem Parameter n

Zunächst wird betrachtet, wie sich die Schwere der Formeln entwickelt, wenn der Parameter nfest gewählt wird. Die Schwere bezeichnet dabei, wie viele Belegungen von einem SAT-Solvergetestet werden müssen, beziehungsweise wieviel Zeit benötigt wird, um eine erfüllende Belegungzu finden. Betrachten wir die Ergebnisse der Tests mit dem Algoritmus von Schöning, die inder Abbildung 5.2 zu finden sind, dann sehen wir für die Konstruktionsvarianten mit und ohneÄquivalenzklauseln eine deutlich unterschiedliche Entwicklung bei einem wachsenden Parameterm. Werden den Formeln Äquivalenzklauseln hinzugefügt, so steigt die Anzahl der im Durchschnittgetesteten Belegungen langsam an und nähert sich später, wenn m bereits ein Vielfaches von mangenommen hat, langsam seinem Maximum. Anders sieht es aus, wenn keine Äquivalenzklauselnhinzugefügt werden, dann ist es für kleine m offenbar sehr einfach für Schönings Algorithmus dieFormeln auf Erfüllbarkeit zu testen. Im nachfolgenden Abschnit werden wir herausfinden, dassder Grund darin liegt, dass diese Formeln sehr viele erfüllende Belegungen besitzen. Bei etwam ≈ n + 1 erfolgt ein schlagartiger Anstieg. Es folgt ein langsamer Abfall und die gemessenenWerte nähern sich nun dem Maximum der Formeln mit Äquivalenzklauseln von der anderen Seitean. Wenn man von dem Anfangsbereich absieht, sind also die Formeln ohne Äquivalenzklauselnvon Schönings Algorithmus deutlich schwerer auf Erfüllbarkeit zu prüfen. Es liegt die Vermutungnahe, dass die Äquivalenzklauseln hilfreich sind, eine erfüllende Belegung zu finden.

13 14 15 16 17 18 19 20 21 22m0.0

0.5

1.0

1.5

2.0

2.5

�Z

eiti

ns

×102

EagleUPsparrowadaptg2wsatsattimeselectorppfolio64

n = 15, N = 180

14 16 18 20 22 24 26 28 30m0.0

0.2

0.4

0.6

0.8

1.0

1.2

1.4

1.6

1.8 ×104

EagleUPsparrowadaptg2wsatsattimeselectorppfolio64plingeling64

n = 20, N = 240

18 20 22 24 26 28 30 32 34m0.0

0.2

0.4

0.6

0.8

1.0

�Z

eiti

ns

×103

ppfolio64plingeling64

n = 25, N = 300

28 30 32 34 36 38 40 42 44m0

1

2

3

4

5

6 ×103

ppfolio64

n = 32, N = 384

Abbildung 5.3: Ergebnisse für SAT-Solver bei Formeln, die durch Vervielfältigung und ohne Äqui-valenzklauseln erzeugt wurden. Der Parameter n ist fest und m ∈ [0, 1].

51

Page 52: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kommen wir nun zu den heuristischen SAT-Solvern, dessen Ergebnisse in Abbildung 5.3 zu findensind. Da die Äquivalenzklauseln offenbar dazu führen, dass die Erfüllbarkeit der Formeln einfa-cher festzustellen ist, wurden hier nur noch Formeln ohne Äquivalenzklauseln getestet. Zwar lösendie heuristischen SAT-Solver das Problem sehr viel schneller und es können Formeln mit bis zu384 Variablen getestet werden, aber es ist eine ähnliche Charakteristik zu beobachten. Es gibt eineSpitze bei m ≈ n + 1 für geringere Anzahl von Variablen (siehe N = 180, 240) und m ≈ n + 2

für eine höhere Anzahl (siehe N = 336, 384). Der Abfall nach der Spitze scheint hier stärker aus-geprägt zu sein, wobei auch bei Schönings Algorithmus schon eine Verstärkung des Abfalls nachder Spitze für ein wachsendes n feststellbar ist. Die Tatsache, dass alle SAT-Solver eine ähnlicheCharakteristik aufweisen, ist ein Argument dafür, dass die Struktur der Formeln dafür ursächlichist.

Analyse des Phasenübergangs

Der Phasenübergang für die hier untersuchte Formelfamilie ist in Abbildung 5.4 in einem Dia-gramm dargestellt. Jeder dargestellte Messpunkt repräsentiert den Anteil der 1000 Formeln, beidenen die erfüllende Standardbelegung (100110010011)n gefunden wurde. Da beim RandomWalk Algorithmus von Schöning (siehe Abschnitt 3.5) die Ausgangsbelegungen für die lokaleSuche zufällig gewählt werden, hat jede erfüllende Belegung einer Formel die gleiche Chance ge-funden zu werden. Demnach können die hier ermittelten Werte als Indikatoren für die Anzahl dererfüllenden Belegungen, die eine Formel besitzt, dienen.

2 4 6 8 10 12

m0.0

0.2

0.4

0.6

0.8

1.0n = 3

f(m, 4.47, 3.05)

n = 4

f(m, 4.52, 4.11)

n = 5

f(m, 3.8, 5.21)

n = 6

f(m, 3.38, 6.27)

n = 7

f(m, 5.17, 7.39)

n = 8

f(m, 3.9, 8.49)

Abbildung 5.4: Phasenübergang bei Formeln, die durch Vervielfältigung und ohne Äquivalenz-klauseln erzeugt wurden. Die Y-Achse gibt an, wie oft anteilig die garantiert existierende, erfül-lende Standardbelegung gefunden wurde.

Wir können für die hier getesteten Formeln einen Bereich festmachen, in dem der Phasenübergangstattfindet. Für etwa m ≤ n− 1 haben die Formeln sehr viele erfüllende Belegungen und für etwam ≥ n+ 1 besitzen sie fast nur noch die eine Standardbelegung. Doch man kann auch sehen, dassder Übergang sich mit wachsendem Parameter n in die Länge zieht, so dass die abgelesenen Gren-zen für deutlich größere n vermutlich keine Gültigkeit haben werden. Dazwischen beobachten wireinen Übergang, wie er von der logistischen Funktion

f(m, a, b) =1

1− ea(b−m)

52

Page 53: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

bekannt ist, wobei der Wert a den Anstieg des Wendepunkts und b die Verschiebung desselbenauf der m Achse definiert. Diese Modellfunktion wurde ebenfalls im Diagramm dargestellt. DieParamter a und b sind jeweils mittels der Methode der kleinsten Quadrate bestimmt worden.

Es lässt sich weiterhin beobachten, dass die Schwere der Formeln für ein festes n ihren maximalenWert an der Stelle m hat, wo der Phasenübergang abgeschlossen ist. Also dort, wo die Formelnanfangen, nur noch eine erfüllende Belegung zu besitzen. In der folgenden Tabelle sind die ermit-telten Paramter der Modellfunktion f für die verschiedenen Formelparameter n zu finden.

n 3 4 5 6 7 8

Wendepunktanstieg a 4,47 4,52 3,8 3,38 5,17 3,9Wendepunktposition b 3,05 4,11 5,21 6,27 7,39 8,49M(b)/N(n) 3,39 3,43 3,47 3,48 3,52 3,54

Tabelle 5.2: Wendepunktposition und Wendepunktansteig bei dem Phasenübergang von Formeln,die durch Vervielfältigung erzeugt wurden, für verschiedene Formelparameter n.

Laufzeitverhalten bei wachsendem Parameter n

Nun wird das Laufzeitverhalten für Schönings Algorithmus und verschiedene andere SAT-Solverin Abhängigkeit zu der Anzahl der Variablen N(n) betrachtet. Für den Parameter n wurde jeweilsder Parameter m so gewählt, dass sich ein maximaler Durchschnittswert ergibt. Welche Wertevon m das im einzelnen sind lässt sich in den Diagrammen oben ablesen. Die Ergebnisse fürmit Schönings Algorithmus sind in Abbildung 5.5 zu finden und die der übrigen SAT-Solver inAbbildung 5.6. Die Y-Achse hat in beiden Fällen eine logarithmische Skalierung.

30 40 50 60 70 80 90 100

N104

105

106

107

108

109

1010

1011

1012

max

m(�

gete

stet

eB

eleg

unge

n)

mit Aquivalenzklauseln3N · 20.286N

ohne Aquivalenzklauseln3N · 20.297N

Abbildung 5.5: Laufzeitverhalten von Schönings SAT-Algorithmus bei Formeln, die durch Ver-vielfältigung erzeugt wurden, in Abhängigkeit der Variablenanzahl N = 12n. Mit und ohne Ver-wendung von Äquivalenzklauseln.

Im Angesicht der Tatsache, dass die getesteten Formeln auf der Basis einer kleinen festen For-mel konstruiert werden, steht die Frage im Raum, ob die Solver es schaffen aus der konstruiertenFormel diese Kopien der kleinen Formel in irgendeiner Weise zu rekonstruieren. Sollte das derFall sein, müsste der Solver nur n-mal eine Formel mit 12 Variablen auf Erfüllbarkeit prüfen undes wäre keine exponentielle Laufzeit in Abhängigkeit zu N(n) zu erwarten, sondern eine poly-

53

Page 54: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

nomielle. Wir sehen an den Ergebnissen, alle verwendeten SAT-Solver haben eine exponentielleLaufzeit, die Tabelle 5.3 liefert genaueres.

0 50 100 150 200 250 300 350 400

N10−4

10−3

10−2

10−1

100

101

102

103

104

105

106

107

max

m(�

Zei

tin

s)

EagleUP0.00002 · 20.123Nsparrow0.00005 · 20.112Nadaptg2wsat0.00030 · 20.106Nsattime0.00049 · 20.102Nselector0.00055 · 20.081Nppfolio640.00002 · 20.072Nplingeling640.00001 · 20.087N

Abbildung 5.6: Laufzeitverhalten der SAT-Solver bei Formeln, die durch Vervielfältigung erzeugtwurden, in Abhängigkeit der Variablenanzahl N = 12n. Ohne Verwendung von Äquivalenzklau-seln.

Dass ppfolio64 am besten abschneidet, was die absoluten Werte betrifft, mag daran liegen, dassdieser Solver ein Multithread-Solver ist und die anderen nur auf einem Prozessor arbeiten kön-nen. Das asymptotische Laufzeitwachstum betrifft das aber nicht. Auch hier liefert ppfolio64 diebesten Werte. Mit Vorsicht muss die ermittelte asymptotische Laufzeit des Solvers selector be-trachtet werden, denn wie im Diagram zu sehen, verläuft diese an der Stelle N = 288 nicht stetig.Da selector auf Basis einer vorhergehenden Analyse der gegebenen Formel eine Auswahl des zuverwendenden Solvers trifft, ist hier zu vermuten, dass selector ab dieser Stelle eine andere Ent-scheidung trifft als zuvor.

ApproximierteSAT-Solver Zeitkomplexität

Schöning (theo. obere Schranke) O(3N · 1,333N )

Schöning mit Äquivalenzklauseln O(3N · 1,219N )

Schöning ohne Äquivalenzklauseln O(3N · 1,229N )

EagleUP O(1,089N )

sparrow O(1,081N )

adaptg2wsat O(1,076N )

sattime O(1,073N )

selector O(1,058N )

ppfolio64 O(1,051N )

plingeling64 O(1,062N )

Tabelle 5.3: Approximierte Zeitkomplexität der SAT-Solver bei Formeln, die durch Vervielfältig-ung erzeugt wurden, in Abhängigkeit der Variablenanzahl N = 12n.

54

Page 55: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Zusammenfassung

Äquivalenzklauseln Die Äquivalenzklauseln, die manchen Formeln hinzugefügt wurden, ga-rantieren, dass diese Formeln nur genau eine erfüllende Belegung besitzen. Allerdings verlierendie Formeln dadurch an Schwere, denn mit Schönings Algorithmus müssen dann im Durchschnittweniger Belegungen getestet werden, um die erfüllende zu finden.

Charakteristik der Formeln Bei festem Parameter n haben die SAT-Solver beim Testen derErfüllbarkeit von Formeln ohne Äquivalenzklauseln eine Spitze was die durchschnitlliche Anzahlgetesteter Belegungen beziehungsweise Zeit betrifft bei grob m ≈ n+ 1, wobei mit steigendem n

dieser Wert sich noch weiter nach Rechts zu verschieben scheint. Die folgende Charakteristik istbei allen SAT-Solvern zu beaobachten.

n+ 1m

Zei

t

Phasenübergang Wählt man den Parameter n fest (und damit auch die Anzahl der VariablenN ) und lässt m wachsen, dann gibt es Phasenübergang von „die Formeln haben sehr viele erfül-lende Belegungen“ zu „die Formeln haben genau eine erfüllende Belegung“. Bei welchem Wertfür m dieser stattfindet, hängt von n ab. Die Schwere der Formeln ist dort maximal, wo der Pha-senübergang fast abgeschlossen ist. Der jeweilige Wert m, wo der Phasenübergang stattfindet unddas entsprechende Verhältnis von Kluaseln zu Variablen lässt sich aus der folgenden Tabelle ent-nehmen.

n 3 4 5 6 7 8

m 3,05 4,11 5,21 6,27 7,39 8,49M(m)/N(n) 3,39 3,43 3,47 3,48 3,52 3,54

Tabelle 5.4: Parameterwerte des Formeltyps, der durch Vervielfältigung generiert wird, wo derPhasenübergang stattfindet.

Laufzeitverhalten Die Vermutung, die SAT-Solver könnten die versteckten Kopien der fes-ten Formel, die zur Konstruktion dieser Formelfamilie verwendet wird, rekonstruieren und sodie Erfüllbarkeit in Polynomialzeit ermitteln, hat sich nicht bestätigt. Alle verwendeten SAT-Solver haben eine exponentielle Laufzeit in Abhängigkeit von N(n). Die asymptotische Laufzeitvon Schönings Algorithmus beträgt O(3N · 1,229N ), wobei die theoretische obere Schranke beiO(3N · 1,333N ) liegt. Der beste heuristische SAT-Solver ppfolio64 erreicht O(1,051N ).

55

Page 56: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

5.5 3-Färbbarkeit von Graphen

Verwendete SAT-Formeln

Alle hier untersuchten Formeln sind gemäß dem Algorithmus ColoringCNF im Abschitt 9 er-stellt worden. Der Algorithmus erhält als Eingabe die Parameter n ∈ N und p ∈ [0, 1] um er-füllbare Formeln durch Reduktion von 3-Färbbarkeit zu generieren. Als Ausgangsgraph dient einzufällig generierter, aber 3-färbbarer Graph mit n Knoten, bei dem jede Kante, die nicht die 3-Färbbarkeitseigenschaft verletzt, mit einer Wahrscheinlichkeit von p existiert. Die Implementie-rung des Konstrunktionsalgorithmus weicht in einem Punkt von der Version im Abschnitt 9 ab.Es wurden als Ausgangsgraphen auch welche mit einer Knotenanzahl, die nicht durch drei teilbarist, verwendet. Die Restknoten sind dann einer beliebigen Menge zugefügt worden. Die Formelnhaben N(n) = 3n Variablen und eine erwartete Anzahl von Klauseln

EW (M(n, p)) = n+ pn2

=N

3+pN2

9.

Für die Untersuchungen mit dem SAT-Algorithmus von Schöning sind Formeln mit den Para-metern N ∈ {30, 33, 36, ..., 120} und p ∈ {0, 0,1, 0,2, 0,3, ..., 1} verwendet worden. Für jedePaarung wurden 100-2000 Formeln erzeugt.

Für die übrigen SAT-Solver wurden zunächst Formeln mit N ∈ {30, 60, 90, ..., 300} und p ∈{0, 0,1, 0,2, 0,3, ..., 1} erstellt. Doch nachdem klar wurde, dass einige Solver diese Formeln sehreffizient auf Erfüllbarkeit prüfen können, wurden weitere Formeln mitN ∈ {300, 450, 600, ..., 1500}generiert.

Die erzeugten Formeln besitzen Klauseln der Länge 3, dessen Aufgabe es ist, zu garantieren, dassjeder Knoten des Ursprungsgraph eine Farbe zugewiesen bekommt, und Klauseln der Länge 2, diesicherstellen, dass zwei benachbarte Knoten nicht gleich gefärbt sind. In diesem Abschnitt wurdenauch zwei Varianten von Schönings Algorithmus verglichen. Die eine bevorzugt bei der Auswahleiner unerfüllten Klausel diejenigen der Länge 3 und die andere diejenigen der Länge 2.

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

�ge

test

ete

Bel

egun

gen

×104

schoening64

N = 60, n = 20

0.0 0.2 0.4 0.6 0.8 1.0p0

1

2

3

4

5

6

7 ×107

schoening64

N = 120, n = 40

Abbildung 5.7: Ergebnisse für Schönings SAT-Algorithmus bei Formeln, die durch 3-Färbbarkeitvon Graphen konstruiert wurden. Der Formelparameter N = 3n ist fest und p ∈ [0, 1].

56

Page 57: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.2

0.4

0.6

0.8

1.0

1.2�

Zeit

ins

×101

selectorsparrow2011ppfolio64plingeling64

N = 900, n = 300

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.5

1.0

1.5

2.0

2.5

3.0 ×101

selectorsparrow2011ppfolio64plingeling64

N = 1500, n = 500

Abbildung 5.8: Ergebnisse für SAT-Solver bei Formeln, die durch 3-Färbbarkeit von Graphenkonstruiert wurden. Der Formelparameter N = 3n ist fest und p ∈ [0, 1].

Ergebnisse und Interpretation

Charakteristik bei festem Parameter n

Die Testergebnisse mit Schönings Algorithmus, die in Abbildung 5.7 zu sehen sind, zeigen, dassfür etwa p < 0.2 die Formeln noch sehr einfach zu erfüllen sind. Danach steigt die Anzahl derim Durchschnitt getesteten Belegungen zunächst stark, danach schwächer an. Die anderen SAT-Solver zeigen eine deutlich andere Charakteristik, wie in Abbildung 5.8 zu sehen ist.

0.0 0.2 0.4 0.6 0.8 1.0p

0.0

0.2

0.4

0.6

0.8

1.0 n = 10

f(p, 16.50, 0.60)

n = 20

f(p, 17.19, 0.42)

n = 30

f(p, 25.24, 0.33)

n = 40

f(p, 31.44, 0.28)

Abbildung 5.9: Phasenübergang bei Formeln, die durch 3-Farbbarkeit von Graphen erzeugt wur-den. Die Y-Achse gibt den Anteil der Tests, in denen eine der sechs garantiert existierende, er-füllende Belegungen gefunden wurde, an. Weiterhin ist eine Modellfunktion mit approximiertenParametern dargestellt.

Analyse des Phasenübergangs

Der Phasenübergang von Formeln mit sehr vielen erfüllenden Belegungen zu Formeln mit in die-sem Fall sechs erfüllenden Belegungen ist in der Abbildung 5.9 dargestellt. Offensichtlich gilt für

57

Page 58: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

das ursprüngliche Problem: Je mehr Kanten eingefügt werden, desto weniger gültige Färbungenbeziehungsweise erfüllende Belegungen gibt es. Ein Zusammenhang mit der Charakteristik ausdem vorherigen Abschnitt ist feststellbar. Bei N = 120 und p ≥ 0,2 beginnt die Anzahl dererfüllenden Belegungen schnell zu sinken und die Anzahl der getesteten Belegungen um eine er-füllende zu finden (siehe vorherigen Abschnitt) steigt an dieser Stelle stark an. Auf der anderenSeite haben wir bei p ≥ 0,5 die minimale Anzahl an erfüllenden Belegungen erreicht, aber dieAnzahl der notwendigen Belegungstests steigt dennoch weiter an. Weiterhin ist zu beobachten,dass der Phasenübergang mit wachsendem N steiler verläuft und früher beginnt.

Anhand der Modellfunktion f , die hier in einer analogen Weise wie in Abschnitt 5.4 verwendetwird, kann der kritische Punkt geschätzt werden, an dem die Anzahl der erfüllenden Belegungenstark abnimmt. Die folgende Tabelle enthält die entsprechenden Werte.

Parameter n 10 20 30 40

Wendepunktanstieg a 16,50 17,19 25,24 31,44Wendepunktposition b 0,60 0,42 0,33 0,28Klauselanzahl EW (M(b)) 70 188 327 488M(b)/N(n) 2,33 3,13 3,63 4,07

Tabelle 5.5: Wendepunktposition und Wendepunktansteig bei dem Phasenübergang von Formeln,die durch 3-Färbbarkeit von Graphen erzeugt wurden, für verschiedene Formelparameter n.

Da die hier verwendeten Ausgangsgraphen eine gewisse Ähnlichkeit mit Zufallsgraphen G (n, p)

aufweisen, können wir hier einige bekannte Eigenschaften von Zufallsgraphen hinzuziehen, umden Verlauf des Phasenübergangs zu verstehen.

Aus Satz 2.3 wissen wir, dass für einen Zufallsgraph G ∈ G (m, q) mit qm > 4,69 die Wahr-scheinlichkeit, dass er eine gültige 3-Färbung besitzt sehr gering ist. Die folgende Tabelle 5.6enthält die so berechneten kritischen Punkte für die hier verwendeten Graphen mit N/3 Knoten.

n 10 20 30 40 300 500

pf = 4,69/n 0,469 0.235 0.157 0.117 0.015 0.009

Tabelle 5.6: Kritischer Punkt an dem die Wahrscheinlichkeit, dass ein Zufallsgraph G (n, p) 3-färbbar ist, von sehr groß zu sehr klein übergeht.

Wir können ablesen, dass diese Werte pf jeweils an der Stelle liegen, kurz bevor die Anzahl dererfüllenden Belegungen stark abnimmt. Vermutlich steuert für p < pf der zufällige Anteil unsererUrsprungsgraphen selbst soch sehr viele gültige Färbungen, beziehungsweise erfüllende Belegun-gen, bei und mit zunehmender Anzahl von Kanten bleibt am Ende nur noch die garantierte gültigeFärbung übrig.

Ein weiterer interessanter Aspekt ist die Frage, ob der Ausgangsgraph für eine Formel zusammen-hängend ist. Denn ist er nicht zusammenhängend, dann zerfällt er in Teilgraphen die unabhängigvoneinander gefärbt werden können. Für die 3-SAT Formeln heißt das, dass die Solver die kleine-ren Teilformeln nacheinander auf Erfüllbarkeit prüfen können, was die Arbeit der Solver deutlicherleichtern sollte. Laut Erdos ist der kritische Bereich, wo ein ZufallsgraphG ∈ G (m, q) von nicht

58

Page 59: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

zusammenhängend in zusammenhängend übergeht bei

(1− ε) lnm

m< q <

(1 + ε) lnm

m.

Nun betrachten wir also den Wert lnN/3N/3 für die hier untersuchten Graphen. Die Ergebnisse sind

in der folgenden Tabelle 5.7 zu finden.

n 10 20 30 40 300 500

pz = (lnn)/n 0,230 0,150 0,113 0,092 0,019 0,012

Tabelle 5.7: Kritischer Punkt an dem die Wahrscheinlichkeit, dass ein Zufallsgraph G (n, p) zu-sammenhängend ist, von sehr klein zu sehr groß übergeht.

Auch hier ist ein Zusammenhang mit der Position des empirisch gemessenen Anstiegs, wo dieAnzahl der erfüllenden Belegungen stark abnimmt, erkennbar.

Laufzeitverhalten in Abhängigkeit zu N

Das Diagramm in der folgenden Abbildung 5.10 zeigt die Anzahl der im Durchschnitt getestetenBelegungen in Abhängigkeit zu der Anzahl der Variablen N für die drei verschiedenen Variantenvon Schönings Algorithmus. Die Variante, bei der zuerst alle Klauseln der Größe 3 erfüllt werden,schneidet hier am besten ab. Offenbar kann es beim 3-Färbbarkeitsproblem sinnvoll sein, immervon einer vollständigen Färbung auszugehen, bevor die Gültigkeit dieser überprüft wird.

30 40 50 60 70 80 90 100 110 120

N102

103

104

105

106

107

108

109

max

p(�

Get

este

teB

eleg

unge

n)

zufallige Klausel3N · 20.160N2-Klauseln zuerst3N · 20.168N3-Klauseln zuerst3N · 20.142N

Abbildung 5.10: Laufzeitverhalten von Schönings SAT-Algorithmus in drei verschiedenen Vari-anten für Formeln in 3-KNF, die von 3-Färbbarkeit von Graphen reduziert wurden. Gemessenwurde die durchschnittliche Anzahl der getesteten Belegungen in Abhängigkeit von N , wobei derParameter p so gewählt wurde, dass dieser Wert maximal ist.

Die heuristisch optimierten SAT-Solver kommen durchweg mit den Formeln dieser Art sehr gutzurecht, wie man an den Testergebnissen in Abbildung 5.11 ablesen kann. Selbst für Formelnmit tausenden Variablen benötigen sie nur wenige Sekunden, um die Erfüllbarkeit festzustellen.

59

Page 60: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Auffällig ist hier, dass der Solver sparrow am besten abschneidet, was die absoluten Werte betrifft,obwohl er nur einen Prozessor und nicht 64, wie plingeling64 und ppfolio64, verwendet. Da dieserSolver auch besonders erfolgreich bei zufälligen SAT Formeln ist, könnte dies ein Hinweis daraufsein, dass die Struktur der Formeln, die hier untersucht werden, Ähnlichkeiten zur Struktur derzufälligen Formeln besitzt.

0 200 400 600 800 1000 1200 1400 1600

N10−3

10−2

10−1

100

101

102

max

p(�

Zeit

ins)

selector3.12382 · 20.0020Nsparrow0.01572 · 20.0033Nplingeling640.18826 · 20.0038Nppfolio640.02172 · 20.0047N

Abbildung 5.11: Laufzeitverhalten von SAT-Solvern für Formeln in 3-KNF, die von 3-Färbbarkeitvon Graphen reduziert wurden. Gemessen wurde die durchschnittliche Zeit in Abhängigkeit vonN , wobei der Parameter p so gewählt wurde, dass dieser Wert maximal ist.

Die durch die Methode der kleinsten Quadrate approximierten, asymptotischen Laufzeiten derSolver befinden sich in der nachfolgenden Tabelle 5.8.

ApproximierteSAT-Solver Laufzeit

Schöning (zufällige Klausel) O(3N · 1,117N )

Schöning (2-Klauseln zuerst) O(3N · 1,123N )

Schöning (3-Klauseln zuerst) O(3N · 1,103N )

selector O(1,0014N )

sparrow O(1,0023N )

plingeling64 O(1,0026N )

ppfolio64 O(1,0033N )

Tabelle 5.8: Approximierte Zeitkomplexitäten in Abhängigkeit der Variablenanzahl N der SAT-Solver bei Formeln, die durch 3-Färbbarkeit von Graphen generiert wurden.

Zusammenfassung

Varianten von Schönings Algorithmus Das Bevorzugen von Klauseln der Größe 3 bei derAuswahl unferfüllter Klauseln scheint ein Vorteil und das Bevorzugen von 2-Klauseln scheintdagegen ein Nachteil zu sein. Übersetzt auf das Urspungsproblem der Färbbarkeit hieße das: Esist besser zunächst eine vollständige Belegung zu wählen, bevor die Gültigkeit überprüft wird.

Phasenübergang Die empirische Untersuchung lässt vermuten: Sowohl der kritische Punkt pf =

qm > 4.69 (siehe [MUL02]), ab dem ein Zufallsgraph G ∈ G (m, q) mit großer Wahrschein-

60

Page 61: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

lichkeit nicht mehr die Eigenschaft der 3-Färbbarkeit besitzt, ist bei den hier behandelten 3-SAT

Formeln bedeutsam, als auch der Übergangsbereich (1−ε) lnmm < pz <

(1+ε) lnmm , in dem G von

nicht zusammenhängend zu zusammenhängend entwickelt. Überschreitet der Formelparameter pdiese kritischen Werte, nimmt die Anzahl der erfüllenden Belegungen stark ab, beziehungsweisedie Wahrscheinlichkeit, eine der sechs versteckten Belegungen zu finden stark zu. Der charakte-ristische Verlauf dieser Wahrscheinlichkeit ist in dem folgenden Diagramm zu sehen.

0 pz pf 1p0

1

Laufzeitverhalten Im Gegensatz zu Schönings SAT-Algorithmus kommen die heuristisch opti-mierten Solver sehr gut mit dieser Formelfamilie zurecht. Die beste approximierte asymptotischeLaufzeit erzielt selector mit O(1,0014N ).

5.6 3-Färbbarkeit von 3-uniformen Hypergraphen

In diesem Abschnitt geht es um die Untersuchung von 3-SAT-Formeln, die durch Reduktion des 3-Färbbarkeitsproblems für semizufällige Hypergraphen konstruiert werden. Zunächst wird auf dieverwendeten Formeln beziehungsweise dessen Parametrisierung eingegangen und es folgt eineAuswertung der experimentellen Untersuchung dieser Formelfamilie. Zuletzt werden die Ergeb-nisse dieses Abschnitts zusammengefasst.

Verwendete Formeln

Es werden Formeln in 3-KNF untersucht, die mit dem Algorithmus HColoringCNF(n, p) ausAbschnitt 9 generiert wurden. Dieser randomisierte Konstruktions-Algorithmus wird durch dieWerte n ∈ N und p ∈ [0, 1] parametrisiert. Als Basis dient bei der Konstruktion ein semizufälligerHypergraph mit n Knoten und einer Kantenwahrscheinlichkeit p, für Kanten, die nicht die 3-Färbbarkeit verletzen. Schließlich erhalten wir Formeln mit N = 3n Variablen, die garantierterfüllbar sind und ausschließlich Klauseln der Länge 3 enthalten.

Es wurden Formeln mit den folgenden Werten für den Parameter p erzeugt:

p ∈ {0; 0,02; 0,04; ...; 0,2; 0,3; 0,4; ...; 1}Für Tests mit Schöning SAT-Algorithmus wurde der Parameter n wie folgt gewählt:

n ∈ {10, 15, 20, 25}Die Tests mit den übrigen SAT-Solver sind mit Formeln durchgeführt worden, für die n wie folgtgewählt wurde:

n ∈ {10, 20, 30, ..., 90}Für alle Paarungen n, p wurden bei Schönings Algorithmus je 500 Formeln generiert und bei denüberigen Solvern je 50.

61

Page 62: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Ergebnisse und Intepretation

Charakteristik in Abhängigkeit zum Parameter p

In den Diagrammen in Abbildung 5.12 ist zu sehen, wie sich die benötigte Anzahl an geteste-ten Belegungen, bis eine erfüllende gefunden wird, in Abhängigkeit zum Parameter p entwickelt.Charakteristisch ist, dass für kleine p schon nach einer geringen Anzahl von getesteten Belegun-gen eine erfüllende gefunden wird, darauf folgt ein Bereich in dem diese Zahl stark ansteigt undschließlich wird ein Wert erreicht, der bis p = 1 nahezu konstant bleibt. Dieser Übergangsbereichist kleiner und findet früher statt, umso größer n.

0.0 0.2 0.4 0.6 0.8 1.0p4.5

5.0

5.5

6.0

6.5

7.0

�ge

test

ete

Bel

egun

gen ×101

schoening64

n = 5, N = 15

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.5

1.0

1.5

2.0

2.5 ×104

schoening64

n = 15, N = 45

0.0 0.2 0.4 0.6 0.8 1.0p0

1

2

3

4

5

6

7 ×106

schoening64

n = 25, N = 75

Abbildung 5.12: Ergebnisse für Schönings SAT-Algorithmus bei Formeln, die durch 3-Färbbarkeitvon Hypergraphen konstruiert wurden. Der Formelparameter N = 3n ist fest und p ∈ [0, 1].

In den nun folgenden Diagrammen in Abbildung 5.13 sehen wir die Testergebnisse der übrigenSAT-Solver. Zu beachten ist, dass hier die Zeit in Abhängigkeit von p gemessen wurde. Auffälligist, dass hier kein konstanter Wert erreicht wird, sondern die Zeit nach einem Sprung am Anfangkontinuierlich ansteigt.

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.2

0.4

0.6

0.8

1.0

1.2

1.4

�Z

eiti

ns

ppfolio64adaptg2wsatMPhaseSATcirminisat

n = 40, N = 120

0.0 0.2 0.4 0.6 0.8 1.0p0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

4.5 ×102

ppfolio64adaptg2wsatMPhaseSATcirminisatselector

n = 90, N = 270

Abbildung 5.13: Ergebnisse für SAT-Solver bei Formeln, die durch 3-Färbbarkeit von Hypergra-phen konstruiert wurden. Der Formelparameter N = 3n ist fest und p ∈ [0, 1].

62

Page 63: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Analyse des Phasenübergangs

Betrachten wir nun, wie der Übergang von „die Formeln hat sehr viele erfüllende Belgungen“zu „sie besitzt nur die eine garantierte erfüllende Belegung“ stattfindet. Dazu wurde mit demSAT-Algorithmus von Schöning gezählt, in wievielen Fällen die bekannte garantierte Belegunggefunden wird. In der folgenden Abbildung ist angegeben wie groß der Anteil ist, in denen dieStandardbelegung gefunden wurde, in Abhängigkeit von p.

0.0 0.1 0.2 0.3 0.4 0.5p

0.0

0.2

0.4

0.6

0.8

1.0 n = 5

f(p, 14.86, 0.218)

n = 10

f(p, 60.33, 0.082)

n = 15

f(p, 187.60, 0.043)

n = 20

f(p, 1252.43, 0.022)

n = 25

f(p, 1407.19, 0.019)

Abbildung 5.14: Phasenübergang bei Formeln, die durch 3-Färbbarkeit von Hypergraphen erzeugtwurden. Die Y-Achse gibt an, wie oft anteilig die garantiert existierende, erfüllende Standardbe-legung gefunden wurde. Außerdem wurde eine Modellfunktion mit approximierten Parameterneingezeichnet.

Anhand der Modellfunktion f , die hier in einer analogen Weise wie in Abschnitt 5.4 verwendetwird, kann der kritische Punkt geschätzt werden, an dem die Anzahl der erfüllenden Belegungenstark abnimmt. Die folgende Tabelle enthält die entsprechenden Werte.

Parameter n 5 10 15 20 25

Wendepunktanstieg a 14,86 60,33 187,60 1252,43 1407,19Wendepunktposition b 0,218 0,082 0,043 0,022 0,019Klauselanzahl EW (M(b)) 11,72 37,56 66 89,42 138,75M(b)/N(n) 0,78 1,25 1,47 1,49 1,85� erfüllte Literale p. Klausel 0,52 0,53 0,55 0,55 0,56

Tabelle 5.9: Wendepunktposition und Wendepunktansteig bei dem Phasenübergang von Formeln,die durch 3-Färbbarkeit von Hypergraphen erzeugt wurden, für verschiedene Formelparameter n.Weiterhin ist angegeben, wie groß der Anteil erfüllter Literale pro Klausel für die entsprechendenFormelparameter und die jeweils gefundene erfüllende Belegung ist.

Es kann beobachtet werden, dass der Wendepunkt sich mit wachsendem Parameter n an den Wertetwa p ≈ 0,017 annähert.

In Satz 2.4 haben wir eine Schranke für die 2-Färbbarkeit von einem zufälligen HypergraphenH ∈ H (m, q, k) kennengelernt, die von der Anzahl der Kanten beziehungsweise von der Kan-tenwahrscheinlichkeit abhängt. Die in diesem Abschnitt behandelten Hypergraphen sind zwar

63

Page 64: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

nicht vollständig mit den zufälligen Hypergraphen identisch, da Kanten, die die 3-Färbbarkeits-eigenschaft verletzen würden, mit Wahrscheinlichkeit 0 statt p existieren. Hinzu kommt, dasswir hier statt dem 2-Färbbarkeitsproblem das 3-Färbbarkeitsproblem betrachten. Dennoch, je-der 2-färbbare Hypergraph ist auch 3-färbbar und das 3-Färbbarkeitsproblem ist genauso NP-vollständig wie es das 2-Färbbarkeitsproblem ist. Die Schranke sollte also geeignet sein, den Ver-lauf des empirisch bestimmten Phasenübergangs in Abbildung 5.14 besser deuten zu können. Diein Satz 2.4 gegebene Schranke lautet

q

(m

k

)≥ 2k−1 ln 2− ln 2

2.

Um die kritischen Punkte im Phasenübergang zu bestimmen, müssen wir also die Ungleichungdurch eine Gleichung ersetzen, q = pk,m = n = N/3 und k = 3 einsetzen und nach p umstellen.

pf =4 ln 2− ln 2

2(N/33

)Für Formeln mit N = 15, 30, 45, 60, 75 erhalten wir nun die folgenden Werte.

n 5 10 15 20 25

pf 0,24260 0,02022 0,00533 0,00213 0,00105

Tabelle 5.10: Der Kritische Punkt, an dem die Wahrscheinlichkeit, dass ein zuffälliger HypergraphH (m, q, k) 2-färbbar ist, von fast 1 zu fast 0 übergeht. Es gilt k = 3.

Vergleicht man diese Berechnungen mit den Stellen im Diagramm, wo ein Anstieg zu verzeichnenist, also wo die Anzahl der erfüllenden Belegungen stark abnimmt, dann kann hier ein Zusammen-hang festgestellt werden. Demnach nimmt die Anzahl der erfüllenden Belegungen im kritischenBereich p ≥ pk stark ab, weil der zufällige Anteil des ursprünglichen Hypergraph, von dem ausge-hend die Formeln generiert werden, selbst immer weniger erfüllende Belegungen produziert, bisschließlich nur die erfüllende Belegung existiert, die Konstruktionsweise bedingt ist. Weiterhin isteben an diesen Stellen zu beobachten, dass die SAT-Solver erhöhten Aufwand betreibem müssen,um die Erfüllbarkeit festzustellen, wie in den Abbildungen 5.12 und 5.13 zu sehen ist.

Laufzeitverhalten in Abhängigkeit zu N

Zuletzt stellt sich die Frage, wieviel Aufwand die SAT-Solver in Abhängigkeit der Anzahl derVariablen N bzw. der Anzahl von Knoten n betreiben müssen, um die Erfüllbarkeit der Formelnfestzustellen. Dabei wurde für jedes N der Parameter p so gewählt, dass die durchschnittlicheAnzahl von getesteten Belegungen oder die durchschnittlich benötigte Zeit maximal ist. Bei denTestergebnissen mit Schönings SAT-Algorithmus, die in Abbildung 5.15 zu sehen sind, entsprichtjeder Messpunkt dem Durchschnitt über 500 Formeln. Die Resultate der übrigen SAT-Solver be-finden sich in Abbildung 5.16. Hier gibt jeder Messpunkt den Durchschnitt über 50 Formeln an.

64

Page 65: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

0 10 20 30 40 50 60 70 80N10−2

10−1

100

101

102

103

104

105

106

107

108

max

p(�

Get

este

teB

eleg

unge

n)schoening643N · 20.2284N

Abbildung 5.15: Laufzeitverhalten von Schönings SAT-Algorithmus für Formeln mit N Varia-blen in 3-KNF, die von 3-Färbbarkeit von Hypergraphen reduziert wurden. Gemessen wurde diedurchschnittliche Zeit in Abhängigkeit von N , wobei der Parameter p so gewählt wurde, dassdieser Durchschnittswert maximal ist.

0 50 100 150 200 250 300N10−2

10−1

100

101

102

103

104

max

p(�

Zei

tin

s)

selector4.41900 · 20.0248Nppfolio640.00860 · 20.0414Nadaptg2wsat0.05400 · 20.0378Nsattime0.07920 · 20.0341Ncirminisat0.01680 · 20.0297NMPhaseSAT0.00950 · 20.0547Nplingeling640.02800 · 20.0760N

Abbildung 5.16: Laufzeitverhalten von SAT-Solvern für Formeln mit N Variablen in 3-KNF, dievon 3-Färbbarkeit von Hypergraphen reduziert wurden. Gemessen wurde die durchschnittlicheZeit in Abhängigkeit von N , wobei der Parameter p so gewählt wurde, dass dieser Durchschnitts-wert maximal ist.

Aus den empirisch bestimmten Laufzeiten der SAT-Solver lässt sich die asymptotische Zeitkom-plexität beziehungsweise bei Schönings Algorithmus die Komplexität der Anzahl der getestetenBelegungen in Abhängigkeit von der Anzahl der Variablen N abschätzen. Dabei wurde für Schö-nings Algorithmus mittels der Modellfunktion 3N · 2aN der Parameter a unter Logarithmierungund durch Minimierung des quadratischen Fehlers approximiert. Für die übrigen Solver wurdec+ d · 2eN mit den Paramtern c, d und e verwendet. So ergeben sich die in der folgenden Tabellegenannten Laufzeitkomplexitäten der SAT-Solver.

65

Page 66: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

ApproximierteSAT-Solver Zeitkomplexität

schoening64 O(3N · 1,172N )

selector O(1.017N )

ppfolio64 O(1.030N )

adaptg2wsat O(1.027N )

sattime O(1.024N )

cirminisat O(1.021N )

MPhaseSAT O(1.039N )

plingeling64 O(1.054N )

Tabelle 5.11: Die Approximierten Zeitkomplexitäten in Abhängigkeit der Variablenanzahl N derSAT-Solver bei Formeln, die durch 3-Färbbarkeit von Hypergraphen erzeugt wurden.

Die Ergebnisse des Solvers sparrow sind hier nicht aufgeführt, weil sie nicht vollständig erhobenwerden konnten. Obwohl dieser Solver in den anderen Experimenten vergleichweise gut abge-schnitten hat, scheint er mit diesem Formeltyp große Probleme zu haben. Für einige Formeln mitzum Beispiel nur 30 Variablen konnte er auch nach tagelanger Laufzeit kein Ergebnis liefern. Obes daran lag, dass die Heuristiken des SLS-basierten Solvers für diesen Formeltyp völlig ungeeig-net sind, oder hier ein Fehler in der Implementierung vorliegt, konnte nicht geklärt werden.

Zusammenfassung

In diesem Abschnitt wurden Formeln experimentell untersucht, die auf Basis von 3-färbbaren Hy-pergraphen konstruiert werden. Durch die Konstruktionsmethode bedingt besitzen diese Formelnimmer zumindest eine erfüllende Belegung.

Wenn der Parameter p und damit die erwartete Anzahl der Kanten des zugrundeliegenden Hy-pergraphen variiert wird, zeigt sich bei Schönings Algorithmus und den übrigen SAT-Solvern einunterschiedliches Bild. Bei Schöning haben wir einen frühen, starken Anstieg der Anzahl der Be-legungstests, der offenbar im Zusammenhang mit dem Phasenübergang steht. Bei den Solvernsehen wir dagegen einen langsamen Anstieg.

Phasenübergang Mit zunehmender Anzahl von Kanten im Hypergraph kommt ein Bereich, indem die Anzahl der erfüllenden Belegungen für die entsprechende aussagenlogische Formel starkabnimmt, bis nur noch die garantierte Belegung erfüllend ist. Dieser Übergang findet umso früherund abrupter statt, desto größer die Anzahl der Knoten. Anhand der empirischen Daten konnte er-mittelt werden, dass dieser kritische Punkt für die Kantenwahrscheinlichkeit sich mit wachsendemParameter n an den Wert etwa p ≈ 0,017 annähert. Es kann weiterhin beobachtet werden, dass ander Stelle qk wo ein zufälliger Hypergraph H ∈ H (m, q, k) mit hoher Wahrscheinlichkeit nichtmehr 2-färbbar ist, auch die Anzahl der erfüllenden Belegungen der reduzierten Formeln starkabnimmt.

Laufzeitanalyse Alle in den Tests verwendeten SAT-Solver haben eine exponentiell wachsendeLaufzeit in Abhängigkeit zur Anzahl der VariablenN . Der SAT-Solver selector hat mitO(1.017N )

66

Page 67: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

die beste asymptotische Laufzeit erreicht.

5.7 Das X3C-Problem

Das X3C-Problem ist ein Spezialfall des Problems der exakten Überdeckung. Gegeben ist eineGrundmengeU und eine Menge S = {S1, S2, ..., Sn} von Teilmengen der Größe 3 vonU soll eineTeilmenge S′ von S gefunden werden, so dass jedes Element von U in genau einem Element vonS′ enthalten ist. Eine ausführliche Beschreibung des Problems und dem allgemeineren Problemder exakten Überdeckung ist in Abschnitt 2.4 zu finden. Hier geht es darum SAT-Formeln, diebasierend auf dem obigen Problem konstruiert werden, experimentell zu untersuchen.

Verwendete Formeln

In diesem Abschnitt werden SAT Formeln in k-KNF beziehungsweise 3-KNF durch Reduktionvom X3C-Problem so erzeugt, dass sie garantiert zumindest eine erfüllende Belegung besitzen.Das genaue Verfahren ist dabei durch den Algorithmus X3CCNF in Abschnitt 8 gegeben. DieParamter n,m ∈ N geben dabei die Größe der Grundmenge |U | = m und die Größe Tripelmenge|S| = n an. Bedingt durch die Art der Reduktion hängt die Anzahl der Variablen einer SAT-Formelin diesem Fall von der Größe der Tripelmenge ab, es gilt N = n.

Es wurden für die Tests mit Schönings SAT-Algorithmus jeweils 10 Formeln für die folgendenParameterpaarungen erzeugt.

n ∈ {3, 6, 9, ..., 120} und

m ∈ {3, 6, 9, ..., 2n} .

Für die übrigen SAT-Solver sind jeweils 150 Formeln mit nachfolgenden Parametern gewählt wor-den.

n ∈ {30, 60, 90, ..., 390} und

m ∈ {3, 9, 15, 21, 27, ..., 3n} .

In beiden Fällen wurden alle Experimente mit den beiden Konstruktionsvarianten durchgeführt.Die erste produziert Formeln, die Klauseln mit bis zu n Literalen enthalten, und die andere er-zwingt eine maximale Klauselgröße von 3.

Ergebnisse und Interpretation

Charakteristik bei festem Paramter n

In den folgenden Dagrammen in Abbildung 5.17 sehen wir, wie sich die durchschnittliche Anzahlder getesteten Belegungen bei Schönings SAT-Algorithmus für Formeln in n-KNF entwickelt,wenn der Parameter n fest und Parameter m wie oben beschrieben variiert wird. Es ist zu beob-achten, dass bei diesen Formeln für die meisten Paarungen von n,m sehr schnell eine erfüllende

67

Page 68: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Belegung gefunden wird, außer um die Stelle etwa m = n/2 herum (gestrichelte vertikale Linie),wo der notwendige Aufwand, um die Erfüllbarkeit festzustellen, plötzlich stark ansteigt.

0 20 40 60 80 100m0.0

0.2

0.4

0.6

0.8

1.0

�ge

test

ete

Bel

egun

gen

×105

n = 60, N = 60

0 20 40 60 80 100m0.0

0.2

0.4

0.6

0.8

1.0

1.2 ×107

n = 90, N = 90

0 20 40 60 80 100m0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

4.5 ×108

n = 120, N = 120

Abbildung 5.17: Ergebnisse für Schönings SAT-Algorithmus bei Formeln mit N Variablen in n-KNF, die durch das X3C-Problem konstruiert wurden. Der Formelparameter N = n ist fest undm ∈ [0, 100]. Die horizontale gestrichelte Linie wurde bei n/2 gezogen.

Bei den Test mit Formeln, die ausschließlich Klauseln mit maximaler Größe drei enthalten, er-kennen wir in Abbildung 5.18 ebenfalls eine Spitze bei etwa n = m/2 (gestrichelte vertikaleLinie), obwohl eine leichte Verschiebung nach links festgestellt werden kann. Aber wir beobach-ten auch, dass im Gegensatz zu den Formeln in n-KNF bei den Spitzen deutlich höhere Werte fürdie im Mittel notwendigen Belegungstests erreicht werden. Die ist zurückzuführen auf die erhöhteAnzahl von Variablen, die bei der Zerlegung einer n-Klausel zu 3-Klauseln enstehen.

0 5 10 15 20 25 30 35 40m0.0

0.5

1.0

1.5

2.0

�ge

test

ete

Bel

egun

gen

×106

n = 30

0 5 10 15 20 25 30 35 40m0.0

0.2

0.4

0.6

0.8

1.0

1.2 ×108

n = 42

0 5 10 15 20 25 30 35 40m0.0

0.2

0.4

0.6

0.8

1.0

1.2 ×1010

n = 54

Abbildung 5.18: Ergebnisse für Schönings SAT-Algorithmus bei Formeln mit N Variablen in 3-KNF, die durch das X3C-Problem konstruiert wurden. Der Formelparameter N = n ist fest undm ∈ [0, 100]. Die horizontale gestrichelte Linie wurde bei n/2 gezogen.

Die Anzahl der Variablen bei einer Formel in 3-KNF hängt nicht allein vom Parameter n oderm ab, sondern von der inividuellen X3C-Instanz, von der sie reduziert wurde. Da diese Instanzenteilweise randomisiert konstruiert werden, variiert die Anzahl der Variablen N und die Anzahlder Klauseln M in den resultierenden SAT-Formeln. Die folgende Tabelle enthält daher für dieParameterpaarungen der beobachteten Spitzen entsprechende Durchschnittswerte, wobei jeweils10 Formeln zugrunde liegen.

68

Page 69: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

n m avg(N) avg(M)

30 12 84,0 338,230 15 54,3 261,030 18 67,7 245,442 18 114,1 466,742 21 105,4 402,042 24 97,1 363,554 24 144,7 600,954 27 135,4 541,954 30 127,9 487,5

Tabelle 5.12: Die Durchschnittliche Variablen- und Klauselanzahl bei Formeln, die durch dasX3C-Problem erzeugt und in 3-KNF umgewandelt wurden, mit den Formelparametern n und m.

In den nun folgenden Diagrammen sind die gleichen Untersuchungen mit den anderen SAT-Solvern durchgeführt worden. Auch hier wurde die vertikale gestrichelte Line wieder beim = n/2

eingezeichnet.

0 50 100 150 200 250m0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

�Ze

itin

s

×101

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 240

0 50 100 150 200 250m0

1

2

3

4

5

6

7

8

9 ×101

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 300

0 50 100 150 200 250m0.0

0.5

1.0

1.5

2.0

2.5

3.0 ×103

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 390

Abbildung 5.19: Ergebnisse für SAT-Solver bei Formeln mitN Variablen in n-KNF, die durch dasX3C-Problem konstruiert wurden. Der Formelparameter N = n ist fest und m ∈ [0, 100]. Diehorizontale gestrichelte Linie wurde bei n/2 gezogen.

0 50 100 150 200 250m0.0

0.2

0.4

0.6

0.8

1.0

1.2

1.4

�Ze

itin

s

×101

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 240

0 50 100 150 200 250m0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5 ×101

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 270

0 50 100 150 200 250m0.0

0.2

0.4

0.6

0.8

1.0

1.2 ×102

selectoradaptg2wsatcirminisatsattimesparrowplingeling64ppfolio64

n = 300

Abbildung 5.20: Ergebnisse für SAT-Solver bei Formeln mit N Variablen in 3-KNF, die durch dasX3C-Problem konstruiert wurden. Der Formelparameter N = n ist fest und m ∈ [0, 100]. Diehorizontale gestrichelte Linie wurde bei n/2 gezogen.

Es ist eine vergleichbare Charakteristik zu erkennen, wie bei den Experimenten mit Schönings

69

Page 70: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

SAT-Algorithmus. Auch hier gibt es eine Spitze in der Nähe von m = n/2, allerdings liegt diesehier nicht genau an diesem Punkt, sondern etwas davor. Ob dies darauf zurückzuführen ist, dasswir uns hier in deutlich größeren Bereichen von n befinden oder ob es an den SAT-Solver selbstliegt, dazu wurde in der folgenden Abbildung 5.21 Schönings Algorithmus den übrigen Solvernbei gleichem Parameter n gegenübergestellt. Die Solver selector und sattime sind hier weggelassenworden, da diese einen sehr großen konstanten Wert in der Laufzeit haben und zum einen keineSpitze mehr auszumachen wahr, zum anderen die Scala der Y-Achse zu stark vergrößert wird.

0 50 100 150 200 250m0.0

0.2

0.4

0.6

0.8

1.0

1.2

1.4

1.6

1.8

�Ze

itin

s

×10−1

adaptg2wsatcirminisatsparrowplingeling64ppfolio64

n = 120, k-KNF, Solver

0 20 40 60 80 100m0.0

0.5

1.0

1.5

2.0

2.5

3.0

3.5

4.0

4.5 ×108

n = 120, k-KNF, Schöning

Abbildung 5.21: Vergleich von Schönings SAT-Algorithmus mit den übrigen SAT-Solvern für For-meln mit n = 120 in n-KNF, die durch X3C-Instanzen konstruiert wurden.

Analyse des Phasenübergangs

Nun soll abgeschätzt werden wieviele erfüllende Belegungen eine Formel besitzt, die mit dem Al-gorithmus X3CCNF(n,m) konstruiert wurde. Dazu wird bei den Tests mit dem SAT-Algorithmusvon Schöning gemessen, wie oft die gefundene erfüllende Belegung einer Formel, derjenigengleicht, die garantiert existiert. Wird diese versteckte Belegung nie gefunden, heißt das, es existie-ren sehr viele erfüllende Belegungen und im ungekehrten Fall, wenn immer die versteckte Bele-gung gefunden wird, kann gefolgert werden, es existiert nur diese eine. Da Schönings Algorithmusein Random Walk Algorithmus ist, hat jede erfüllende Belegung die gleiche Wahrscheinlichkeitgefunden zu werden und es können Schlussfolgerungen dieser Art getroffen werden. Die gemes-senen Werte deuten darauf hin, dass der Phasenübergang, also der Übergang von „es wird sehrselten die versteckte Belegung gefunden“ zu „es wird immer die versteckte Belegung gefunden“,gemäß der folgenden Gesetzmäßigkeit verläuft.

f(q, a, b) =1

1− ea(b−q)

Es handelt sich hierbei um die logistische Funktion, mit den Parametern a und b. Der Parametera bestimmt die Steigung des Wendepunkts und der Parameter b die Position des Wendepunkts.Die logistische Funktion wird hier als Modellfunktion für die Methode der kleinsten Quadrateverwendet. In der folgenden Abbildung 5.22 sind die Anteile zu sehen, wie oft der Algorithmusvon Schöning die versteckte erfüllende Belegung findet, und der entsprechende Verlauf der Mo-dellfunktion mit den approximierten Parametern.

70

Page 71: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

0 20 40 60 80 100

m0.0

0.2

0.4

0.6

0.8

1.0n = 30

f(m, 0.47, 14.91)

n = 45

f(m, 0.32, 23.84)

n = 60

f(m, 0.29, 29.23)

n = 75

f(m, 0.47, 33.38)

n = 90

f(m, 0.23, 39.18)

n = 105

f(m, 0.23, 46.67)

n = 120

f(m, 0.3, 51.32)

Abbildung 5.22: Phasenübergang bei Formeln, die durch das X3C-Problem erzeugt wurden. DieY-Achse gibt an, wie oft anteilig die garantiert existierende, erfüllende Standardbelegung gefun-den wurde. Desweiteren wurde jeweils eine Modellfunktion mit approximierten Parametern ein-gezeichnet.

In der folgenden Tabelle 5.13 sind die approximierten Parameter mit den zugehörigen Formelpa-rametern aufgeführt.

n 30 45 60 75 90 105 120

n/2 15 22,5 30 37,5 45 52,5 60Steigung a 0,47 0,32 0,29 0,47 0,23 0,23 0,3Wendepunkt b 14,91 23,84 29,23 33,38 39,18 46,67 51,32� erfüllte Literale p. Klausel 0,81 0,80 0,82 0,83 0,84 0,83 0,83

Tabelle 5.13: Die Wendepunktposition und der Wendepunktansteig bei dem Phasenübergang vonFormeln, die durch das X3C erzeugt wurden, für verschiedene Formelparameter n.Weiterhin istangegeben, wie groß der Anteil erfüllter Literale pro Klausel für die entsprechenden Formelpara-meter und die jeweils gefundene erfüllende Belegung ist.

Es ist zu beobachten, dass der Wendepunkt immer kurz vor dem Wert m = n/2 liegt. Also kurzvor der Stelle, bei der die obigen Untersuchungen zeigten, dass dort die Schwierigkeit, die Formelnauf Erfüllbarkeit zu testen, stark ansteigt.

Das X3C lässt sich auf das Cliquenproblem reduzieren, indem jedes Tripel der Menge S einenKnoten darstellt und zwei Knoten miteinander durch eine Kante verbunden sind, wenn die ent-sprechenden Tripel keine gemeinsamen Elemente besitzen. Wir können daher Kenntnisse über dieExistenz von Cliquen in Zufallsgraphen nutzen, um Aussagen über zufällige X3C-Instanzen zutreffen und die hier gewonnenen Ergebnisse besser zu verstehen. Dabei müssen wir jedoch be-rücksichtigen, dass die hier untersuchten X3C-Instanzen nur teilweise zufällig sind, da sie stetseine garantierte Lösung besitzen und weiterhin die Eigenschaft eines Zufallsgraphen, dass jedeKante unabhängig von den anderen Kanten mit einer gewissen Wahrscheinlichkeit existiert, hierebenfalls nicht ganz zutrifft.

In einem von einer X3C-Instanz mit |U | = m reduzierten Graphen G ist die Kantenwahrschein-

71

Page 72: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

lichkeit p gleich der Wahrscheinlichkeit, dass zwei zufällig gewählte Tripel keine gemeinsamenElemente besitzen, also

p(m) =m− 3

m· m− 4

m− 1· m− 5

m− 2.

Die Wahrscheinlichkeit, dass dieser Zufallsgraph in Gn,p eine Clique der Größe k enthält, erhaltenwir durch Multiplikation der Anzahl der möglichen Kombinationen von k aus n Knoten

(nk

)mit

der Wahrscheinlichkeit, dass alle Kanten zwischen ihnen existieren und erhalten so

z(n, k, p) =

(n

k

)p

k(k−1)2 .

Da wir in X3C-Instanzen nach einer exakte Abdeckung der größe m/3 suchen, müssen wir auchin G nach einer Clique der größe m/3 suchen. Wir wählen also k = m/3. Die entsprechendenWerte können dem nachfolgenden Diagramm in Abbildung 5.23 entnommen werden.

0 20 40 60 80 100 120 140

m0.0

0.2

0.4

0.6

0.8

1.0n = 30

f(m, 0.47, 14.91)

z(30,m/3, p(m))

n = 60

f(m, 0.29, 29.23)

z(60,m/3, p(m))

n = 90

f(m, 0.23, 39.18)

z(90,m/3, p(m))

Abbildung 5.23: Empirisch bestimmter Phasenübergang (Messpunkte; Anteil der garantiert exis-tierenden Standardbelegung unter allen erfüllenden Belegungen) inklusive approximierter Mo-dellfunktion f (durchgezogene Linie) und die Wahrscheinlichkeit z einer k-Clique (gestrichelteLinie).

Wir sehen hier als durchgezogene Linie den Anteil der Tests, bei denen die garantierte erfüllendeBelegung beziehungsweise die garantiert exakte Abdeckung von Schönings SAT-Algorithmus ge-funden wird. Das heißt, ein kleiner Wert lässt auf sehr viele erfüllende Belegungen schließen undein großer Wert nahe 1 auf sehr wenige. Die gestrichelte Linie ist die Wahrscheinlichkeit einerk-Clique. Wenn also die Wahrscheinlichkeit einer k-Clique groß ist, sollte man annehmen, dassdie Anzahl der erfüllenden Belegungen groß ist, da neben der versteckten Belegung auch die zu-fällig enstandenen hinzukommen. Dagegen, wenn die Wahrscheinlichkeit einer k-Clique klein ist,sollte nur die garantierte erfüllende Belegung verbleiben. Im Diagramm lässt sich ablesen, dassder Punkt, an dem der Anteil, den die versteckten Belegung ausmachen, stark zunimmt mit demPunkt, wo die Wahrscheinlichkeit einer k-Clique stark abnimmt, korreliert.

Laufzeitwachstum in Abhängigkeit der Variablenzahl N

In den hier folgenden Diagrammen ist die Laufzeitkomplexität der verschiedenen SAT-Algorith-men in Abhängigkeit zu der Anzahl von Variablen für die verschiedenen Varianten der Formeln zu

72

Page 73: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

sehen. Bei Schönings SAT-Algorithmus wurde wieder die Anzahl der getesteten Belegungen stattder tatsächlichen Zeit als Maß verwendet. In Abbildung 5.24 sind die Testergebnisse für SchöningsSAT-Algorithmus mit den Formel in n-KNF und 3-KNF zu sehen. Für die übrigen SAT-Solverwurden die Ergebnisse für die beiden Formelvarianten getrennt dargestellt, sie befinden sich inAbbildung 5.25 und 5.26.

0 20 40 60 80 100 120

N10−1

1001011021031041051061071081091010

max

m(�

Get

este

teB

eleg

unge

n) schoening, 3-KNF3N · 20.175Nschoening, n-KNF3N · 20.175N

Abbildung 5.24: Laufzeitverhalten von Schönings SAT-Algorithmus für Formeln mit N = n Va-riablen in n-KNF und 3-KNF, die vom X3C-Problem reduziert wurden. Gemessen wurde diedurchschnittliche Zeit in Abhängigkeit von N , wobei der Parameter m so gewählt wurde, dassdieser Durchschnittswert maximal ist.

0 50 100 150 200 250 300 350 400

N10−3

10−2

10−1

100

101

102

103

104

max

m(�

Zeit

ins)

selector3.70731 · 20.015Nadaptg2wsat0.00006 · 20.066Ncirminisat0.00000 · 20.071Nsattime0.00018 · 20.058Nsparrow0.00020 · 20.055Nplingeling640.00047 · 20.042Nppfolio640.00005 · 20.048N

Abbildung 5.25: Laufzeitverhalten von SAT-Solvern für Formeln mit N = n Variablen in n-KNF,die vom X3C-Problem reduziert wurden. Gemessen wurde wieder die durchschnittliche Zeit inAbhängigkeit von N , wobei m so gewählt wurde, dass der Wert maximal ist.

Die höhere Streuung, die bei Tests mit Schönings SAT-Algorithmus mit Formeln in 3-KNF zubeobachten ist, kommt dadurch zustande, dass, wie bereits oben erwähnt, die Anzahl der Variablen

73

Page 74: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

N bei diesen Formeln etwas vom Zufall abhängt und sich daher die 10 Formeln eines Messpunktsauf verschiedene N verteilen, im Gegensatz zu den Formeln in n-KNF. Die Ergebnisse zeigen,dass Schönings Algorithmus die Erfüllbarkeit der Formeln nicht schneller ermitteln kann, wennein Teil der Variablen dem Zwecke der Klauselzerlegung dient.

0 200 400 600 800 1000 1200 1400 1600 1800

N10−3

10−2

10−1

100

101

102

max

m(�

Zeit

ins)

selector5.05118 · 20.0Nadaptg2wsat0.02501 · 20.003Ncirminisat0.00670 · 20.003Nsattime0.03303 · 20.003Nsparrow0.00662 · 20.005Nplingeling640.04110 · 20.003Nppfolio640.00866 · 20.002N

Abbildung 5.26: Laufzeitverhalten von SAT-Solvern für X3C-Formeln mit N = n Variablen inn-KNF. Es wurde die durchschnittliche Zeit in Abhängigkeit von N gemessen, der Parameter mwurde dabei so gewählt, dass dieser Durchschnittswert maximal ist.

Die übrigen SAT-Solver kommen mit solchen Variablen, die in eine Formel eingefügt werden,um große Klauseln in 3-Klauseln zu zerlegen, sehr gut zurecht, wie wir bei den Ergebnissen mitFormeln in 3-KNF in der Abbildung 5.26 beobachten können. Die Laufzeiten sind deutlich besserbei den Formeln in n-KNF bei gleicher Anzahl von Variablen N . Weiterhin können wir hier einebogenförmige Struktur erkennen, die darauf zurückzufühen ist, dass wir für Formeln in 3-KNF mitParameter n, Formeln mit unterschiedlicher Variablenanzahl N bekommen, insbesondere, wennder Parameter m variiert. Das heißt, die Methode, die m für ein festes N so auszuwählen, dassdie Zeit maximal ist, trägt hier nicht, da sich die Formeln für ein festes n auf verschiedene Nverteilen. Daher können wir jede dieser bogenförmigen Strukturen einem Wert für den Parametern zuordnen.

Alternativ könnte man hier zunächst die Werte für ein festes n bestimmen und dann die Zeitenfür ein durchschnittliches N ins Diagramm eintragen. Das würde allerdings die Messergebnisseverfälschen, da es sich bei der Durchschnittsfunktion um eine lineare Abbildung handelt, die Zeitaber exponentiell in Abhängigkeit zu N wächst.

Aus den experimentell bestimmten Laufzeiten ergeben sich die in der folgenden Tabelle 5.14dargestellten approximierten Zeitkomplexitäten.

74

Page 75: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Approximierte ApproximierteSAT-Solver Zeitkomplexität n-KNF Zeitkomplexität 3-KNF

schöning O(3N · 1,129N ) O(3N · 1,129N )

selector O(1,010N ) siehe Abbildung 5.26adaptg2wsat O(1,047N ) O(1,002N )

cirminisat O(1,050N ) O(1,002N )

sattime O(1,041N ) O(1,002N )

sparrow O(1,039N ) O(1,003N )

plingeling64 O(1,030N ) O(1,002N )

ppfolio64 O(1,034N ) O(1,001N )

Tabelle 5.14: Die approximierten Zeitkomplexitäten in Abhängigkeit der Variablenanzahl N derSAT-Solver bei Formeln, die durch das X3C-Problem erzeugt wurden.

Zusammenfassung

Es wurden SAT-Formeln auf Basis des X3C-Problems randomisiert konstruiert und experimentelluntersucht. Eine X3C-Instanz (U, S) mit der Grundmenge U und der Tripelmenge S wird aufeine SAT-Formel in n-KNF mit N = n = |S| Variablen reduziert. Zerlegt man zusätzlich dien-Klauseln in 3-Klauseln, entstehen weitere Variablen.

Charakteristik Wählt man den Parameter n fest und variiert m = |U | ergibt sich folgendescharakteristisches Bild.

n/2m

Zeit

Allerdings verschiebt sich der kritische Punkt m = n/2 bei größeren Werten für n leicht nachlinks.

Phasenübergang Es findet auch hier ein Phasenübergang von „die Formeln hat sehr viele er-füllende Belegungen“ zu „die Formel hat nur eine erfüllende Belegung“ statt, der vom Formel-parameter m abhängt. Durch Reduktion von X3C auf CLIQUE kann man (teilweise) zufälligeX3C-Instanzen mit Zufallsgraphen vergleichen. Der Punkt, an dem für eine durch X3C konstru-ierte Formel die Anzahl der erfüllenden Belegungen abnimmt korreliert mit dem Punkt, an demdie Wahrscheinlichkeit für eine entsprechend große Clique in einem Zufallsgraph abnimmt.

Laufzeitanalyse Die SAT-Solver haben ein exponentielles Laufzeitwachstum in Abhängigkeitzur Anzahl der Variablen N . Bei der Formelvariante in 3-KNF stellen die neu hinzugekommenenVariablen für keinen der Solver außer Schönigs SAT-Algorithmus eine nennenswerte Erhöhung

75

Page 76: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

der Schwierigkeit dar, so dass Formeln in 3-KNF statt n-KNF deutlich effizienter auf Erfüllbarkeitgeprüft werden können.

5.8 Teilgraph-Isomorphie

Verwendete Formeln

Bei den Formeln die durch TICNF (siehe Abschnitt 14) basierend auf dem Teilgraph-Isomorphie-Problem konstruiert werden, haben wir die drei Formelparameter n,m, p. Der Parameter n be-stimmt die Anzahl der Knoten, die zunächst in den zwei isomorphen Graphen enthalten sind. DerParameter m bestimmt wieviele Knoten dann einem der beiden Graphen noch hinzugefügt wer-den und p ist die Wahrscheinlichkeit der Existenz jeder Kante, die nicht die Teilgraph-Isomorphieverletzt. Es wurden Formeln mit n = 7, 8, 9, m = 0, 1, 2, ..., 2n und p = {0; 0,2; 0,4; 0,6; 0,8, 1}erzeugt. Und zwar 50 für jede Parameterkombination.

Ergebnisse und Interpretation

Charakteristik bei festem Parameter n

Nachfolgend in Abbildung 5.27 sind die Ergebnisse zu sehen, die Schönings SAT-Algorithmusliefert, wenn der Parameter n fest gewählt wird. Es muss allerdings berücksichtigt werden, dasssich die Anzahl der Variablen N bei den resultierenden Formeln mit Vergrößerung des Parametersm ebenfalls vergrößert. Wir können einen starken Anstieg der im Mittel getesteten Belegungenbei n = 8,m = 8, p = 0,4 und n = 9,m = 12, p = 0,2 beobachten.

m

02468101214

16

p

0.00.2

0.40.6

0.81.0

.

�getestete

Belegungen

×10

6

0

1

2

3

4

5

n = 8

m

024681012141618

p

0.00.2

0.40.6

0.81.0

.

�getestete

Belegungen

×10

8

0.0

0.2

0.4

0.6

0.8

1.0

1.2

n = 9

Abbildung 5.27: Ergebnisse für Schönings SAT-Algorithmus bei Formeln, die durch Reduktionvom Teilgraph-Isomorphie-Problem konstruiert wurden. Der Formelparameter n ist fest, m ∈[0, 2n] und p ∈ [0, 1].

76

Page 77: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Analyse des Phasenübergang

Auffalland ist hier, dass in dem Bereich des Parameterraums, wo die meisten Belegungen gestes-tet werden müssen (siehe Oben), die Anzahl der erfüllenden Belegungen dennoch sehr hoch ist,wie die folgende Abbildung 5.28, die angibt, wie oft die versteckte erfüllende Belegung anteiliggefunden wird, zeigt. Das die Anzahl von Variablen mit wachsendem m steigt, wird dabei eineRolle spielen.

m

024681012

1416

18

p

0.00.2

0.40.6

0.81.0

×10 −

1

0

1

2

3

4

5

6

7

8

9

n = 7

n = 8

n = 9

Abbildung 5.28: Phasenübergang bei Formeln, die durch das Teilgraph-Isomorphie-Problem er-zeugt wurden. Die Y-Achse gibt an, wie oft anteilig die garantiert existierende, erfüllende Stan-dardbelegung gefunden wurde.

5.9 Vergleich der Formelfamilien

In diesem Abschnitt soll die Schwere der verschiedenen Formelfamilien abgeschätzt werden, in-dem die Laufzeiten der SAT-Solver in Abhängigkeit der Variablenanzahl gegenüber gestellt wer-den. Die jeweiligen Formelparameter, die die Anzahl der Klauseln bestimmen, werden stets sogewählt, dass die Laufzeit des entsprechenden Solvers maximal wird. Für diese festen Parameterwurde dann ein Durchschnittswert über bestimmte Anzahl von Formel ermittelt. Daher sprechenwir hier auch von einem Worst-Case-Durchschnitt. Bei Schönings SAT-Algorithmus sind nicht dieZeiten gemessen worden, sondern die Anzahl der Belegungstests, die notwendig waren, bis eineerfüllende Belegung gefunden wurde.

Die gestrichelten Linien in den folgenden Diagrammen geben die durch Minimierung des quadra-tischen Fehlers approximierte asymptotische Zeitkomplexität für die jeweilige Formelfamilie undden jeweiligen Solver an. Näheres dazu in Abschnitt 5.3.

Als Referenzgröße dienen hier Zufallsformeln in 3-KNF mit M = 4,2N , wobei die nicht erfüll-baren Formeln zuvor herausgefiltert wurden.

77

Page 78: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Schönings SAT-Algorithmus

Der SAT-Algorithmus von Schöning erzielt die besten Ergebnisse bei den Formeln in 3-KNF, dievon 3-Färbbarkeitsproblem reduziert worden sind. Erstaunlicherweise liefert er auch bei X3C-Formeln, die nicht in 3-KNF sondern in n-KNF befinden, vergleichbare Ergebnisse. Da bei dieserFormelart der Parameter n gleich der Anzahl der Variablen N ist, würde man hier deutlich höhereLaufzeiten erwarten. Denn Schönings k-SAT-Algorithmus hat für große k eine Laufzeit nahe bei2N (vgl. Tabelle 3.1). Dann folgen die Formeln, die auf dem 3-Färbbarkeitsproblem für Hypergra-phen basieren und am schwersten Fallen dem Algorithmus mit Abstand der Formeltyp, der durchdas Kopieren der Klauseln einer Basisformel konstruiert wird. Keinen großen Unterschied gibt eszwischen den beiden Varianten, mit und ohne Äquivalenzklausen, dieser Konstruktionsmethode.

0 20 40 60 80 100 120 140

N1001011021031041051061071081091010101110121013

�W

orst

Cas

e1A

nzah

lget

este

terB

eleg

ugne

n

Klauselkopien (ohne Ak.)3N · 20.3054N

Klauselkopien (mit Ak.)3N · 20.2883N3-Farbbarkeit3N · 20.1598NHyp. 3-Farbbarkeit3N · 20.2284NX3C (n-KNF)3N · 20.1752Nerfullbare Zufallsformeln3N · 20.1956N

Abbildung 5.29: Das Laufzeitverhalten (hier durchschnittle Anzahl getesteter Belegung) vonSchönings SAT-Algorithmus in Abhängigkeit der Variablenanzahl N bei verschiedenen Formel-typen. 1) siehe Abschnitt 5.3

sparrow

Bei dem SAT-Solver sparrow bekommen wir folgendes Bild: die Formeln, die auf dem 3-Färb-barkeitsproblem basieren, sind offenbar noch einfacher auf Erfüllbarkeit zu prüfen, als es bei zu-fälligen, erfüllbaren Formeln der Fall ist. Wie bereits in Abschnitt 5.6 ausgeführt, konnten mitdiesem Solver keine vollständigen Daten für die Formeln basierend auf Hypergraphfärbbarkeiterhoben werden.

78

Page 79: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

0 100 200 300 400 500 600

N10−3

10−2

10−1

100

101

102

103

104

105

106�

Wor

stC

ase1

Zei

tin

sKlauselkopien0.00029 · 20.0995N3-Farbbarkeit0.01011 · 20.0039NX3C (n-KNF)0.00099 · 20.0473Nerfullbare Zufallsformeln0.01537 · 20.0092N

Abbildung 5.30: Das Laufzeitverhalten des SAT-Solvers sparrow in Abhängigkeit der Variablen-anzahl N bei verschiedenen Formeltypen. 1) siehe Abschnitt 5.3

selector

Bei dem Solver selector beobachten wir, dass es Sprünge in Laufzeit gibt. Das liegt daran, dass esein Portfolio-Solver ist, der sich aufgrund einer Analyse der Eingabeformel einen Solver auswählt.So kann es vorkommen, dass bei wachsender Anzahl von Variablen die Entscheidung auch malanders auswällt.

0 100 200 300 400 500 600

N100

101

102

103

104

105

106

�W

orst

Cas

e1Z

eiti

ns

Klauselkopien0.33900 · 20.0450N3-Farbbarkeit3.81027 · 20.0018NHyp. 3-Farbbarkeit4.41903 · 20.0248NX3C (n-KNF)3.28731 · 20.0161Nerfullbare Zufallsformeln3.07151 · 20.0077N

Abbildung 5.31: Das Laufzeitverhalten des SAT-Solvers selector in Abhängigkeit der Variablen-anzahl N bei verschiedenen Formeltypen. 1) siehe Abschnitt 5.3

79

Page 80: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

ppfolio64

Der Solver ppfolio64 lieferte zwar in absoluten Zahlen die besten Werte, aber was die Asymptotikbetrifft finden wir auch hier ein ähnliches Bild, wie bei den übrigen Solvern.

0 100 200 300 400 500 600

N10−3

10−2

10−1

100

101

102

103

104

�W

orst

Cas

e1Z

eiti

ns

Klauselkopien0.00005 · 20.0674N3-Farbbarkeit0.01515 · 20.0052NHyp. 3-Farbbarkeit0.01043 · 20.0400NX3C (n-KNF)0.00058 · 20.0370Nerfullbare Zufallsformeln0.00480 · 20.0136N

Abbildung 5.32: Das Laufzeitverhalten des SAT-Solvers ppfolio64 in Abhängigkeit der Variablen-anzahl N bei verschiedenen Formeltypen. 1) siehe Abschnitt 5.3

plingeling64

Bei dem SAT-Solver plingeling64 kann eine leicht abweichende Situation festgestellt werden. Die-ser Solver scheint größere Schwierigkeiten mit Zufallsformeln zu haben, was daran liegen mag,dass plingeling64 ein DPLL-basierter Solver ist. Aber auch hier gilt, Hypergraph-Färbbarkeit unddie vervielfältigten Formeln stellen die schwersten dar.

0 100 200 300 400 500 600

N10−3

10−2

10−1

100

101

102

103

104

105

106

�W

orst

Cas

e1Z

eiti

ns

Klauselkopien0.00084 · 20.0657N3-Farbbarkeit0.12322 · 20.0044NHyp. 3-Farbbarkeit0.02797 · 20.0760NX3C (n-KNF)0.01321 · 20.0272Nerfullbare Zufallsformeln0.00803 · 20.0270N

Abbildung 5.33: Das Laufzeitverhalten des SAT-Solvers plingeling64 in Abhängigkeit der Varia-blenanzahl N bei verschiedenen Formeltypen. 1) siehe Abschnitt 5.3

80

Page 81: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Kapitel 6

Abschlussdiskussion und Ausblick

Neue Methode erfüllbare Formeln zu konstruieren. Die von Prof. Reischuk vorgeschlageneMethode zur randomisierten Konstruktion schwieriger, erfüllbarer 3-SAT-Formeln mit N Varia-blen und M Klauseln wurde in dieser Arbeit ausgearbeitet und experimentell untersucht. DasKonstruktionsverfahren basiert auf einer festen Basisformel (siehe Anhang), dessen Klauseln ver-vielfältigt und die Literale innerhalb der Kopien randomisiert vertauscht werden. Wenn die Kon-struktionsparameter N,M so gewählt werden, dass grob M/N & 3,47 gilt, dann sinkt die Anzahlder erfüllenden Belegungen sehr stark, bis die Formeln mit an 1 grenzender Wahrscheinlichkeit nurnoch die eine garantiert existierende, erfüllende Belegung besitzen. Weiterhin haben die Untersu-chungen in dieser Arbeit gezeigt: wenn die Konstruktionsparameter an dem genannten kritischenPunkt liegen, haben sowohl die SLS-basierten als auch die DPLL-basierten SAT-Solver eine ex-ponentielle Laufzeit in Abhängigkeit von N , die asymptotisch größer ist, als bei den übrigen indieser Arbeit untersuchten Formeltypen. Zwar sind bereits Konstruktionsmethoden bekannt, diebestimmte SAT-Solving-Methoden austricksen und so die Laufzeit bei der entsprechenden Grup-pe von Solvern in die Höhe treiben können, aber bei diesen Formeln deuten die empirischen Da-ten darauf hin, dass diese im Allgemeinen schwer auf Erfüllbarkeit zu prüfen sind. Die Tatsache,dass diese Formeln randomisiert, garantiert erfüllbar und anscheinend schwer auf Erfüllbarkeitzu testen sind, macht sie zu geeigneten Testformeln für die Weiterentwicklung von SAT-Solvern,insbesondere von unvollständigen.

Untersuchung und Vergleich verschiedener Formeltypen. In dieser Arbeit wurden neben derneuen Formel-Konstruktionsmethode auch die natürlichen NP-vollständigen Probleme 3-Färb-barkeit bei Graphen, 3-Färbbarkeit bei Hypergraphen, das Problem der exakten Überdeckung unddas Teilgraph-Isomorphie-Problem mit Hilfe von optimierten SAT-Solvern experimentell unter-sucht. Für jedes der Probleme wurden randomisiert positive Instanzen generiert und zu erfüllbarenSAT-Formeln in KNF mit N Variablen reduziert. Die Tabelle 6.1 zeigt eine Übersicht der ge-nannten Formeltypen. Der kritische Punkt bezeichnet dabei den Bereich im Parameterraum, wodie Anzahl der erfüllenden Belegungen stark abnimmt. Weiterhin ist jeweils angegeben, wie großder durchschnittliche Anteil an erfüllten Literalen pro Klausel für eine erfüllende Belegung einerentsprechenden Formel am genannten kritischen Punkt ist.

Phasenübergang Bei diesen randomisierten Konstruktionsmethoden von SAT-Formeln konntefestgestellt werden, dass ein sogenannter Phasenübergang existiert. Je nach Wahl der Konstruk-

81

Page 82: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Ausgangs- Vervielfältigung Graph- Hypergraph- X3C Zufalls-problem einer Basisformel Färbbarkeit Färbbarkeit formeln

Parameter n: Klauselkopien n: Knotenanz. n: Knotenanz. n: Tripelanz. n: Variablenm: Auswahlgröße p: Kantenws. p: Kantenws. m: Grundmenge m: Klauseln

Variablenanzahl 12n 3n 3n n n

Klauselanzahl 40m n+ pn2 n+3p((n3)−3(

n33 ))≤ m+

(n2

)m

Kritischer Punkt1 MN ≈ 3,47 0,2← p 0,017← p m ≈ n/2 M

N ≈ 4,2

Erfüllte Literale 0,51667 ≈ 0,63 ≈ 0,55 ≈ 0,82 ≈ 0,55pro Klausel2 (nur Erfüllbare)

Tabelle 6.1: Übersicht der Formelfamilien. 1) Am kritischen Punkt nimmt die Anzahl der erfüllen-den Belegungen stark ab. Die Pfeilschreibweise symbolisiert eine Annäherung dieses Punktes vonRechts an den entsprechenden Wert für eine wachsende Variablenanzahl. 2) Es wurde der durch-schnittliche Anteil erfüllter Literale pro Klausel für eine Belegung einer Formel am kritischenPunkt angegeben.

tionsparameter haben die Formeln entweder sehr viele erfüllende Belegungen oder nur die einegarantierte erfüllende Belegung (es kann auch mehrere garantierte erfüllende Belegungen geben).Dann gibt es den meist sehr kleinen kritischen Bereich im Parameterraum, wo die Anzahl dererfüllenden Belegungen stark abnimmt. Die kritischen Bereiche konnten experimentell bestimmtwerden. Gerade in diesem Bereich, so zeigen die experimentellen Untersuchungen, ist es beson-ders schwer für die Solver, die Erfüllbarkeit festzustellen. Weiterhin wurden Zusammenhänge deremprisch bestimmten Punkte mit theoretischen Eigenschaften von Zufallsgraphen bzw. Zufallshy-pergraphen, wie Färbbarkeit oder Existenz einer k-Clique, disktutiert werden (siehe 5.5, 5.6 und5.7).

Laufzeitanalyse von Schönings SAT-Algorithmus Die Schärfe der theoretischen oberen Schran-ke O(3N · 1,334N ) für die Zeitkomplexität von Schönings SAT-Algorithmus für Eingabeformelnin 3-KNF mit N Variablen, konnte experimentell nicht gezeigt werden. Für alle in dieser Arbeituntersuchten Formelfamilien, die mit Schönings Algorithmus getestet worden sind, wurde eineapproximierte Laufzeit erreicht, die asymptotisch kleiner ist, als die theoretische Schranke, wie inTabelle 6.2 zu sehen ist. Wir können daher schließen, dass die untersuchten Formeln nicht den beiSchönings Analyse betrachteten Worst-Case darstellen. Auf die Gründe soll hier nochmal zusam-menfassend eingegangen werden. Schönings Algorithmus wählt ausgehend von einer zufälligenBelegung eine nicht erfüllte k-Klausel. Aus dieser wird zufällig ein Literal gewählt und die Be-legung der zugrundeliegenden Variable negiert. Sofern eine erfüllende Belegung existiert, beträgtdie Wahrscheinlichkeit, durch so einen lokalen Suchschritt die Hamming-Distanz zur erfüllen-den Belegung um 1 zu veringern, zumindest 1/k, da eines der Literale in der Klausel durch dieerfüllende Belegung erfüllt sein muss. Der Worst-Case wäre also eine Formel, die genau eine er-füllende Belegung besitzt und in jeder Klausel genau ein Literal durch diese erfüllt wird. Für diein dieser Arbeit untersuchten Formeln ist diese Eigenschaft nicht erfüllt (siehe Tabelle 6.1, Zeile„erfüllte Literale pro Klausel“). Auch hätten DPLL-Solver mit einer solchen Formel eine günstigeAusgangsposition, denn die Anzahl positiver und negativer Literale befindet sich notwendiger-weise im Ungleichgewicht (oder die Formel besitzt sehr viele Belegungen), was dazu führt, dassein DPLL-basierter Solver schneller auf Konflikte stößt und so der zu durchsuchende Raum der

82

Page 83: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

geschätzteFormeltyp Zeitkomplexität

Klauselkopien (ohne Äk.) O(3N · 1,229N )

Klauselkopien (mit Äk.) O(3N · 1,219N )

Hypergraph 3-Färbbarkeit O(3N · 1,172N )

X3C (n-KNF) O(3N · 1,129N )

X3C (3-KNF) O(3N · 1,129N )

3-Färbbarkeit (2-Klauseln zuerst) O(3N · 1,123N )

3-Färbbarkeit O(3N · 1,117N )

3-Färbbarkeit (3-Klauseln zuerst) O(3N · 1,103N )

Tabelle 6.2: Empirisch bestimmte Zeitkomplexitäten von Schönings SAT-Algorithmus bei ver-schiedenen Formeltypen und dessen Varianten.

Belegungen sich verkleinert. Betrachten wir die Wahrscheinlichkeit, bei der lokalen Suche aufdas „richtige Literal“ zu stoßen, wie in Tabelle 6.1 angegeben, und vergleichen diese Werte mitden Zeitkomplexitäten in Tabelle 6.2, so können wir einen Zusammenhang feststellen. Diese Da-ten zeigen: je größer die Wahrscheinlich das „richtige Literal“ (bzw. der durchschnittliche Anteilerfüllter Literale pro Klausel) auszuwählen, desto kleiner die asymptotische Laufzeit.

Die Analyse von Schönings Algorithmus mittels Markowketten in Abschnitt 3.5 zeigt, dass beider lokalen Suchstrategie auch weniger als 3N Schritte ausreichend sind, doch eine Verbesserungder asymptotischen Exponentialzeit kann aus dieser Erkenntnis nicht abgeleitet werden, denn dazu Beginn der lokalen Suche erwartungsgemäß die hälfte der Variablenbelegungen richtig geratenwerden, sind zumindest N/2 Suchschritte notwendig.

0 100 200 300 400 500 600

N10−3

10−2

10−1

100

101

102

103

104

�W

orst

Cas

e1Z

eiti

ns

Klauselkopien0.00005 · 20.0674N3-Farbbarkeit0.01515 · 20.0052NHyp. 3-Farbbarkeit0.01043 · 20.0400NX3C (n-KNF)0.00058 · 20.0370Nerfullbare Zufallsformeln0.00480 · 20.0136N

Abbildung 6.1: Dieses Diagramm zeigt die Laufzeit des SAT-Solvers ppfolio64 für verschiedeneFormeltypen in Abhängigkeit der Anzahl der Variablen N . Es zeigt eine Situation, wie sie auchbei den anderen SAT-Solvern typisch ist. 1) siehe Abschnitt 5.3

Schwere der Formeltypen in Abhängigkeit der Variablenanzahl. Zuletzt sollen hier die ver-schiedenen Formeltypen in Bezug auf die Laufzeit der optimierten SAT-Solver in Abhängigkeitder Anzahl der VariablenN verglichen werden. Die Formelparameter sind dabei für jedesN so ge-

83

Page 84: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

wählt, dass bei festem N eine maximale Laufzeit erreicht wird. Die verwendeten Solver liefertendabei ein recht ähnliches Bild der Situation. Nachfolgend sind daher exemplarisch die Ergebnis-se des SAT-Solvers ppfolio64 in Abbildung 6.1 dargestellt. Als Referenzgröße zu den Formel-Konstruktionsmethoden sind erfüllbare Zufallsformeln dargestellt. Es ist deutlich zu sehen, dassdie für Zufallsformeln optimierten Solver größere Schwierigkeiten mit den, in dieser Arbeit unter-suchten, semizufälligen Formeln haben, abgesehen von denjenigen, die durch 3-Färbbarkeit vonGraphen erzeugt werden.

Die folgende Tabelle 6.3 enthält die empirisch bestimmen, asymptotischen Laufzeiten der ver-schiedenen Solver für die jeweiligen Formeltypen.

Formeltyp ppfolio64 selector sparrow plingeling64

Klauselkopien O(1,051N ) O(1,058N ) O(1,081N ) O(1,062N )

3-Färbbarkeit O(1,0033N ) O(1,0014N ) O(1,0023N ) O(1,0026N )

Hyp. 3-Farbbarkeit O(1.030N ) O(1.017N ) (siehe 5.6) O(1.054N )

X3C (n-KNF) O(1,034N ) O(1,010N ) O(1,039N ) O(1,030N )

X3C (3-KNF) O(1,001N ) (siehe Abb. 5.26) O(1,003N ) O(1,002N )

Tabelle 6.3: Die Übersicht der approximierten Zeitkomplexitäten der SAT-Solver bei den ver-schiedenen Formeltypen in Abhängigkeit der Variablenanzahl N . Die Zahl 64 im Solvernamenbedeutet, dass dieser mit 64 parallelen Threads ausgeführt wurde.

6.1 Offene Fragen

Aus den Ergebnissen dieser Arbeit haben sich weitere interessante Fragestellungen ergeben, dieim Rahmen dieser Masterarbeit nicht mehr weiter verfolgt werden konnten. Hier soll kurz aufeinige dieser offenen Fragen eingegangen werden.

Worst-Case Formeln für Schönings SAT-Algorithmus. Es wurde festgestellt, dass bei Schö-nings Algorithmus eine erfüllbare Formel in KNF im Worst-Case genau eine erfüllende Belegungbesitzt und in jeder Klausel genau ein Literal durch diese Belegung erfüllt ist. Weiterhin ist ge-schlussfolgert worden, dass ein DPLL-basierter Solver, aufgrund des Ungleichgewichts positiverund negativer vorkommender Literale, die Frage nach der Erfüllbarkeit schneller lösen kann. Wieausgeprägt dieser Effekt tatsächlich ist, wurde in dieser Arbeit nicht weiter untersucht.

Stochastische Analyse der neuen Formel-Konstruktionsmethode. Die in dieser Arbeit vor-gestellte Methode konstruiert beliebig große Formeln auf Basis einer festen Basisformel, dessenKlauseln randomisiert vervielfältigt werden. Eine insteressante Frage ist, wieviel Information überdie Basisformel in den generierten Formeln steckt. Ein speziell angepasster SAT-Solver, der esschafft die Basisformel anhand der erzeugten Formeln zu ermitteln, könnte diese in Polynomial-zeit auf Erfüllbarkeit prüfen.

Austausch der Basisformel. Die Vervielfältigungsmethode zur Konstruktion von Formeln ba-siert auf der, im Anhang angegebenen, festen 3-SAT-Formel. Das Verfahren könnte aber auch mit

84

Page 85: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

anderen Basisformeln durchgeführt werden. Interessant wäre es, dieses Verfahren mit charakteris-tisch unterschiedlichen Formeln durchzuführen und die Ergebnisse zu vergleichen.

Untersuchung der Abhängigkeitsgraphen der Formeln. Wenn ein SAT-Algorithmus, wie zumBeispiel der von Schöning, durch einen lokalen Suchschritt eine Klausel in der Eingabeformel er-füllt, werden dadurch mit recht hoher Wahrscheinlichkeit andere Klauseln, die zuvor erfüllt waren,nun unerfüllt sein. Solche Abhängigkeiten können durch einen Abhängigkeitsgraphen dargestelltwerden. Eine Möglichkeit ist: es ergeben sich die Knoten aus den Klauseln und Kanten existieren,sofern in den entsprechenden zwei Klauseln zueinander komplementäre Literale vorkommen. DieUntersuchung der Eigenschaften solcher Graphen, für verscheidene Arten von Formeln, könnteweiteren Aufschluss darüber geben, was das SAT-Problem hartnäckig macht.

85

Page 86: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

86

Page 87: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Anhang A

Anhang

A.1 Basisformel

Nachfolgend eine aussagenlogische Formel in 3-KNF mit 12 Variablen, 40 Klauseln mit je genaudrei Literalen. Sie stammt aus den Vorlesungsunterlagen von Prof. Reischuk.

(x1 ∨ x2 ∨ x9) ∧ (x5 ∨ x6 ∨ x7) ∧ (x3 ∨ x4 ∨ x10) ∧ (x3 ∨ x9 ∨ x12) ∧(x3 ∨ x8 ∨ x11) ∧ (x1 ∨ x5 ∨ x10) ∧ (x1 ∨ x6 ∨ x11) ∧ (x1 ∨ x7 ∨ x11) ∧(x2 ∨ x5 ∨ x9) ∧ (x2 ∨ x8 ∨ x9) ∧ (x1 ∨ x3 ∨ x5) ∧ (x8 ∨ x10 ∨ x11) ∧(x2 ∨ x8 ∨ x10) ∧ (x3 ∨ x5 ∨ x9) ∧ (x1 ∨ x9 ∨ x12) ∧ (x2 ∨ x3 ∨ x6) ∧(x2 ∨ x10 ∨ x11) ∧ (x2 ∨ x4 ∨ x5) ∧ (x8 ∨ x9 ∨ x12) ∧ (x4 ∨ x7 ∨ x9) ∧(x3 ∨ x5 ∨ x8) ∧ (x5 ∨ x8 ∨ x10) ∧ (x4 ∨ x6 ∨ x7) ∧ (x6 ∨ x7 ∨ x12) ∧(x4 ∨ x5 ∨ x7) ∧ (x6 ∨ x8 ∨ x12) ∧ (x2 ∨ x6 ∨ x12) ∧ (x8 ∨ x11 ∨ x12) ∧(x7 ∨ x9 ∨ x10) ∧ (x6 ∨ x7 ∨ x8) ∧ (x4 ∨ x6 ∨ x11) ∧ (x1 ∨ x7 ∨ x12) ∧(x7 ∨ x10 ∨ x11) ∧ (x4 ∨ x9 ∨ x12) ∧ (x2 ∨ x4 ∨ x12) ∧ (x3 ∨ x10 ∨ x11) ∧(x1 ∨ x3 ∨ x10) ∧ (x2 ∨ x4 ∨ x11) ∧ (x1 ∨ x4 ∨ x5) ∧ (x1 ∨ x3 ∨ x6)

Für diese Formel existiert genau eine erfüllende Belegung, sie ist in der Tabelle A.1 angegeben.

x1 = 1 x5 = 1 x9 = 0

x2 = 0 x6 = 0 x10 = 0

x3 = 0 x7 = 0 x11 = 1

x4 = 1 x8 = 1 x12 = 1

Tabelle A.1: Die einzige erfüllende Belegung der obigen Basisformel.

Die Anzahl der Literale, die in jeder Klausel durch die obige Belegung erfüllt werden, ist in dernachfolgenden Tabelle angegben. Es wurde dabei die obige Reihenfolge der Klauseln werwendet.

87

Page 88: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

1 1 1 11 1 1 11 2 2 21 2 2 31 2 2 21 1 1 12 2 2 33 1 1 12 1 1 11 2 3 2

Tabelle A.2: Anzahl durch die erfüllende Belegung erfüllter Literale in den Klauseln der Basisfor-mel. Durchschnitt pro Klausel: 1,55 erfüllte Literale (bzw. anteilig 0,51667).

A.2 Inhalt der beigelegten CD

Der vorliegenden Arbeit wurde eine Daten-CD beigelegt, auf der diverse Implementierungen, dieverwendeten SAT-Solver, die gesammelten Rohdaten und diese Arbeit in digitaler Form enthaltensind.

Implementierungen der Formel-Konstruktionsverfahren Die im Kapitel 4 beschriebenen ran-domisierten Konstruktionsverfahren von aussagenlogischen Formeln in KNF wurden in dieser Ar-beit in der Programmiersprache C++ implementiert. Für jedes Verfahren wurde ein eigenständigesUnix-Kommandozeilenprogramm entwickelt, dass als Eingabe die entsprechenden Formelpara-meter erhält und mittels einem randomisierten Prinzip eine Formel konstruiert, die im DIMACS-Format auf die Standardausgabe ausgegeben wird. Wenn beim Ausführen kein Kommandozeilen-parameter angegeben wird, so produzieren die Programme einen Hilfetext, in denen die jeweili-gen Parameter erläutert sind. Neben den Formelparametern kann durch den Parameter -s eineSaat für den Pseudozufallsgenerator angegeben werden. Ohne Angabe dieses Parameters wird deraktuelle Zeitstempel des Systems verwendet. Die Quelltexte dieser Programme sind im Ordnersat-tools auf der CD enthalten, wobei jedes Programm einen eigenen Unterordner besitzt indem sich die entsprechenden Quelltextdateien befinden und ein Kompilationsskript. Im Hauptord-ner befindet sich wiederum ein Kompilationsskript, dass die Skripte in den Unterordner aufruft,um alle Programme auf einen Schlag zu übersetzen. Die ausführbaren Binärdateien werden dannim Unterordner bin abgelegt. Weiterhin existiert ein Unterordner inc in dem sich eine KlasseCNF und weitere nützliche Unterprogramme befinden, die bei einigen der beschriebenen Kon-struktionsverfahren zum Einsatz kommen.

Implementierung von Schönings SAT-Algorithmus Ebenfalls in dem Ordner sat-toolsbefindet sich der für diese Arbeite implementierte SAT-Algorithmus von Schöning. Er wurde auchin C++ programmiert und ist ein Unix-Kommandozeilenprogramm. Die Eingabeformel, die sichim DIMACS-Format befinden muss, kann auf zwei verschiedenen Wegen dem Programm überge-ben werden. Entweder wird sie auf die Standardeingabe des Pogramms geschrieben oder sie wirdin einer Datei abgelegt und der Dateiname wird als Kommandozeilenparameter übergeben. Aus-gegeben wird einerseits, ob die Eingabeformel erfüllbar ist und welche die gefundene erfüllende

88

Page 89: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Belegung ist. Das Ausgabeformat entspricht dabei dem Format, wie es bei den SAT Competiti-ons vorgeschrieben ist. Der Quelltext und das Kompilationsskript befindet sich im Unterordnerschoening. Da nicht alle verwendeten Bibliotheken auf dem Testsystem zur Verfügung stan-den, wird das Programm in zwei verscheidenen Varianten kompiliert. In der normalen Variantewerden die Bibliotheken zur Laufzeit dynamisch nachgeladen und in der statischen Variante sindsie fest einkompiliert. Neben vielen Standardbibliotheken kamen auch GMP und OpenMP zumEinsatz. Bei Schönings Algorithmus muss die Anzahl der Neustarts der lokalen Suche berechnetund auch mitgezählt werden. Diese Zahl kann aber schnell so groß werden, dass die Standardda-tentypen nicht mehr ausreichen und es zu Fehlern im Programm kommen kann. Daher wurde fürden Umgang mit beliebig großen, ganzen Zahlen die GNU Multiple Precision Arithmetic Libra-ry (kurz: GMP) verwendet. Um die 64 Prozessorkerne des Testsystems auszunutzen, wurde derAlgorithmus mit Hilfe der Open Multi-Processing-Bibliothek (kurz: OpenMP) parallelisiert.

SAT-Solver der SAT Competition 2011 Bei den in dieser Arbeit durchgeführten experimen-tellen Untersuchungen wurden SAT-Solver ausgewählt die an der SAT Competition 2011 teilge-nommen und dabei auch gute Plätze erreicht haben. Weiterhin musste beachtet werden, dass dieSolver auf dem Testsystem lauffähig sind und dass möglichst welche mit verschiedenen Ansätzenzu Verfügung stehen (vgl. Kapitel 3). Die ausgewählten Solver werden im Abschnitt 3.8 beschrie-ben. Alle Solver erhalten als Eingabe eine Datei, die eine Formel im DIMACS-Format enthält,in Form des als Kommandozeilenparameter übergebenen Dateinamen. Sie liefern ihr Ergebnis alsstandardisierte Ausgabe auf der UNIX-Standardausgabe. Zwar wurden auch im Jahren 2013 und2014 SAT Competitions durchgeführt, doch die Implementierungen der Solver wurden in diesenJahren nicht veröffentlich. Die statischen ausführbaren Binärdateien aller Solver, die an der SATCompetition 2011 teilgenommen haben, befinden sich auf der CD in dem Ordner SATSolver.

Automatisierte Tests Bei den experimentellen Untersuchungen in dieser Arbeit wurden die im-plementierten Formelkonstruktionsverfahren verwendet, um unterschiedlich parametriesierte For-meln mit den ausgewählten SAT-Solvern auf Erfüllbarkeit zu prüfen und dabei verschiedene Daten,wie zum Beispiel Laufzeit, getestete Anzahl von Belegungen und gefundene erfüllende Belegun-gen, zu sammeln. Dazu wurden für jedes Konstruktionsverfahren Programme in der SkriptsprachePython entwickelt zur massenhaften Produktion von Formeln und zum automatisierten Testen die-ser Formeln mit den verschiedenen SAT-Solvern. Dabei war es notwendig, die in Maschinenspra-che vorliegenden Konstruktionsverfahren und SAT-Solver in die Pythonskripte zu integrieren. Diesgeschah, indem sie mittels dem Pythonmodul subprocess als Unterprozess aufgerufen wurden.Die Kommunikation findet dabei über Kommandozeilenparameter und Standardein- und ausgabestatt. Da neben den parallelisierten SAT-Solvern auch sequentielle Solver zur Verfügung standenwurden zwei Arten von automatisierten Tests durchgeführt. Bei den parallelisierten Solvern wur-den alle Paarungen der zu testenden Formeln und Solver nacheinander abgearbeitet, wobei demjeweiligen Solverprozess alle Prozessorkerne zur Verfügung standen. Bei den sequentiellen Sol-vern wurde eine Warteschlange mit allen Paarungen aufgebaut, die von den 64 Prozessorkernenparallel zueinander abgearbeitet wurden. Es liefen also 64 Tests zeitgleich, wobei jedem Solver-prozess ein Prozessorkern zur Verfügung stand. Die entsprechenden Quelltexte befinden sich indem Ordner Experimente.

Auswertungsprogramme für die gesammelten Daten Für jede erzeugte Formelinstanz wur-den die nachfolgenden Daten erhoben und in SQLite Datenbank gesammelt.

89

Page 90: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

• verwendete Formelparameter

• verwendetes Konstruktionsverfahren

• verwendeter SAT-Solver

• Anzahl der zur Verfügung gestandenen Prozessorkerne

• gemessene Laufzeit des Solvers

• ggf. Anzahl der getesteten Belegungen

• gefundene erfüllende Belegung

• ggf. Übereinstimmung mit der formelspezifischen Standardbelegung

Diese Daten wurden wurden auf unterschiedliche Weise weiterverarbeitet und in den meisten Fäl-len in Diagrammen dargestellt. Hierbei kamen die Pythonwerkzeuge NumPy, SciPy, Matplotlib,PyPlot und so fort zum Einsatz. Die Pythonskripte zur Auswertung der Daten und Generierungder Diagramme befinden sich ebenfalls im Ordner Experimente. Die Datenbankdateien sind indiesem Ordner unter den Namen result.sqlite und iso.sqlite zu finden.

90

Page 91: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Abbildungsverzeichnis

3.1 Beispielhafte Ausführung des DPLL-Algorithmus . . . . . . . . . . . . . . . . . 23

3.2 Schönings lokale Suche modelliert als Markowkette . . . . . . . . . . . . . . . . 28

3.3 Die Wahrscheinlichkeit für den Erfolg Schönings lokaler Suche . . . . . . . . . . 29

4.1 Modellierung der Diskrepanz einer ±1-Sequenz als Zustandsautomat . . . . . . 42

5.1 Beispiel für das DIMACS-Format . . . . . . . . . . . . . . . . . . . . . . . . . 47

5.2 Schönings Algorithmus bei vervielfältigten Formeln mit festem n . . . . . . . . 50

5.3 SAT-Solver bei vervielfältigten Formeln mit festem n . . . . . . . . . . . . . . . 51

5.4 Phasenübergang bei vervielfältigten Formeln . . . . . . . . . . . . . . . . . . . 52

5.5 Laufzeitverhalten der Schönings Algorithmus bei vervielfältigten Formeln . . . . 53

5.6 Laufzeitverhalten der SAT-Solver bei vervielfältigten Formeln . . . . . . . . . . 54

5.7 Schönings Algorithmus bei 3-Färbbarkeit mit festem n . . . . . . . . . . . . . . 56

5.8 SAT-Solver bei 3-Färbbarkeit mit festem n . . . . . . . . . . . . . . . . . . . . . 57

5.9 Phasenübergang bei 3-Farbbarkeits-Formeln . . . . . . . . . . . . . . . . . . . . 57

5.10 Laufzeitverhalten von Schönings SAT-Algorithmus bei 3-Färbbarkeits-Formeln . 59

5.11 Laufzeitverhalten von SAT-Solvern bei 3-Färbbarkeits-Formeln . . . . . . . . . . 60

5.12 Schönings Algorithmus bei Hypergraph-Färbbarkeit mit festem n . . . . . . . . 62

5.13 SAT-Solver bei Hypergraph-Färbbarkeit mit festem n . . . . . . . . . . . . . . . 62

5.14 Phasenübergang bei Hypergraph-Färbbarkeits-Formeln . . . . . . . . . . . . . . 63

5.15 Laufzeitverhalten von Schönings Algorithmus bei Hypergraph-Färbbarkeit . . . . 65

5.16 Laufzeitverhalten von SAT-Solvern bei Hypergraph-Färbbarkeit . . . . . . . . . 65

5.17 Schönings Algorithmus bei X3C-Formeln in n-KNF mit festem n . . . . . . . . 68

5.18 Schönings Algorithmus bei X3C-Formeln in 3-KNF mit festem n . . . . . . . . 68

5.19 SAT-Solver bei X3C-Formeln in n-KNF mit festem n . . . . . . . . . . . . . . . 69

91

Page 92: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

5.20 SAT-Solver bei X3C-Formeln in 3-KNF mit festem n . . . . . . . . . . . . . . . 69

5.21 Vergleich von Schönings SAT-Algorithmus mit SAT-Solvern . . . . . . . . . . . 70

5.22 Phasenübergang bei X3C-Formeln . . . . . . . . . . . . . . . . . . . . . . . . . 71

5.23 Empirischer Phasenübergang gegenüber Wahrscheinlichkeit einer k-Clique . . . 72

5.24 Laufzeitverhalten von Schönings Algorithmus bei X3C-Formeln . . . . . . . . . 73

5.25 Laufzeitverhalten von SAT-Solvern bei X3C-Formeln in n-KNF . . . . . . . . . 73

5.26 Laufzeitverhalten von SAT-Solvern bei X3C-Formeln in 3-KNF . . . . . . . . . 74

5.27 Schönings Algorithmus bei TI-Formeln mit festem n . . . . . . . . . . . . . . . 76

5.28 Phasenübergang bei TI-Formeln . . . . . . . . . . . . . . . . . . . . . . . . . . 77

5.29 Vergleich der Laufzeit von Schönings Algorithmus bei verschiedenen Formeltypen 78

5.30 Vergleich der Laufzeit von sparrow bei verschiedenen Formeltypen . . . . . . . . 79

5.31 Vergleich der Laufzeit von selector bei verschiedenen Formeltypen . . . . . . . . 79

5.32 Vergleich der Laufzeit von ppfolio64 bei verschiedenen Formeltypen . . . . . . . 80

5.33 Vergleich der Laufzeit von plingeling64 bei verschiedenen Formeltypen . . . . . 80

6.1 Vergleich der Laufzeit von ppfolio64 bei verschiedenen Formeltypen . . . . . . . 83

92

Page 93: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Tabellenverzeichnis

3.1 Theoretische Laufzeiten für Schönings SAT-Algorithmus . . . . . . . . . . . . . 26

5.1 Daten des AMD Opteron 6272 Prozessors . . . . . . . . . . . . . . . . . . . . . 48

5.2 Wendepunkte im Phasenübergang bei vervielfältigten Formeln . . . . . . . . . . 53

5.3 Zeitkomplexität der SAT-Solver bei vervielfältigten Formeln . . . . . . . . . . . 54

5.4 Phasenübergangs-Parameter bei vervielfältigten Formeln . . . . . . . . . . . . . 55

5.5 Wendepunkte im Phasenübergang bei 3-Färbbarkeits-Formeln . . . . . . . . . . 58

5.6 Kritischer Punkt der Färbbarkeit von Zufallsgraphen . . . . . . . . . . . . . . . 58

5.7 Kritischer Punkt des Zusammenhangs von Zufallsgraphen . . . . . . . . . . . . 59

5.8 Zeitkomplexitäten der SAT-Solver bei 3-Färbbarkeit . . . . . . . . . . . . . . . . 60

5.9 Wendepunkt des Phasenübergang bei Hypergraph-Färbbarkeit . . . . . . . . . . 63

5.10 Kritischer Punkt der 2-Färbbarkeit von zufälligen Hypergraphen . . . . . . . . . 64

5.11 Zeitkomplexitäten der SAT-Solver bei Hypergraph-Färbbarkeit . . . . . . . . . . 66

5.12 Durchschnittliche Variablen- und Klauselanzahl bei X3C-Formeln in 3-KNF . . . 69

5.13 Wendepunkt des Phasenübergang bei X3C-Formeln . . . . . . . . . . . . . . . . 71

5.14 Zeitkomplexitäten der SAT-Solver bei X3C-Formeln . . . . . . . . . . . . . . . 75

6.1 Übersicht der untersuchten Formelfamilien . . . . . . . . . . . . . . . . . . . . 82

6.2 Empirisch bestimmte Zeitkomplexitäten von Schönings SAT-Algorithmus . . . . 83

6.3 Übersicht der Zeitkomplexitäten der Solver für die Formeltypen . . . . . . . . . 84

A.1 Erfüllende Belegung der Basisformel . . . . . . . . . . . . . . . . . . . . . . . . 87

A.2 Anzahl erfüllter Literale in den Klauseln der Basisformel . . . . . . . . . . . . . 88

93

Page 94: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

94

Page 95: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Algorithmenverzeichnis

1 3ColorableGraph (n, p): Konstruktion 3-färbbarer Zufallsgraphen . . . . . . 35

2 ColoringTo3SAT ((V,E)): Reduktion von 3-Färbbarkeit auf 3-SAT . . . . . . 36

3 ColoringCNF (n, p): Zufällige 3-SAT-Formeln durch 3-Färbbarkeit . . . . . . . 36

4 3ColorableHGraph (n, p): Konstruktion zufälliger, 3-färbbarer Hypergraphen 37

5 HColoringTo3SAT ((V,E)): Reduktion Hypergraph-Färbbarkeit auf 3-SAT . . 38

6 HColoringCNF (n, p): Zufällige 3-SAT-Formeln durch Hypergraph-Färbbarkeit 38

7 X3CInstance (n, m): Zufällige positive X3C-Instanzen . . . . . . . . . . . . . 39

8 X3CToSAT ((U, S)): Reduktion von X3C auf k-SAT . . . . . . . . . . . . . . . 39

9 X3CCNF (n, m): Zufällige k-SAT-Formeln durch X3C . . . . . . . . . . . . . . . 40

10 TIInstance (n, m, p): Konstruktion zufälliger positiver TI-Instanzen . . . . . . 40

11 TIToSAT (G, H): Reduktion von TI auf k-SAT . . . . . . . . . . . . . . . . . . 41

12 TICNF (n, m, p): Konstruktion zufälliger k-SAT-Formeln durch TI . . . . . . . . 42

13 EDPKNF (k): Konstruktion von k-SAT-Formeln durch EDP . . . . . . . . . . . . . 43

14 Klauselkopien (F , n, k): Zufällige 3-SAT-Formeln durch Vervielfältigung . . 44

15 RandomCNF (F , n, k): Zufällige Formeln in 3-KNF . . . . . . . . . . . . . . . . 45

95

Page 96: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

96

Page 97: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

Literaturverzeichnis

[ACH02] Achlioptas, D., Moore, C. (2002), On the 2-colorability of random hypergraphs, Ran-domization and Approximation Techniques in Computer Science, Volume 2483 of the seriesLecture Notes in Computer Science, Seiten 78-90.

[BAL11] Balint, A., Fröhlich, A., Tompkins, D. A. D., Hoos, H. H. (2011) Sparrow2011, SolverDescription, SAT 2011 Competition Booklet.

[BAL13] Balint, A., Belov, A., Heule, M. J. H., Järvisalo, M. (2013), Proceedings of SAT Com-petition 2013: Solver and Benchmark Descriptions, Department of Computer Science Seriesof Publications B, Vol. B-2013-1, University of Helsinki.

[BEL14] Belov, A., Diepold, D., Heule, M. J. H., Järvisalo, M. (2014), Proceedings of SAT Com-petition 2014: Solver and Benchmark Descriptions, Department of Computer Science Seriesof Publications B, Vol. B-2014-2, University of Helsinki.

[BIE09] Biere, A., Heule, M., van Maaren, H., Walsh, T. (2009), Handbook of Satisfiability, IOSPress.

[BIE11] Biere, A., (2011), Lingeling and Friends at the SAT Competition 2011, Technsi-cher Bericht, März 2011, Johannes Kepler Universität, Linz, http://fmv.jku.at/papers/Biere-FMV-TR-11-1.pdf.

[BIR02] Birolia, G., Coccob, S., Monasson, R. (2002), Phase transitions and complexity in com-puter science: an overview of the statistical physics approach to the random satisfiabilityproblem, Physica A: Statistical Mechanics and its Applications, Volume 306, 2002, Seiten381-394.

[BOL01] Bollobás, B. (2001), Random Graphs, Second Edition, Cambridge University Press.

[CHE11] Chen, J. (2011), Phase Selection Heuristics for Satisfiability Solvers, http://arxiv.org/abs/1106.1372.

[COO71] Cook, S. A. (1971), The complexity of theorem-proving procedures, Proceedings of the3rd Annual ACM Symposium on the Theory of Computing (STOC’71), ACM, New York,Seiten 151-158.

[COR09] Cormen, T. H., Leiserson, C. E., Rivest, R. L., Stein, C. (2009), Introduction to Algo-rithms, 3rd edition, MIT Press.

[DP60] Davis, M., Putnam, H. (1960), A computing procedure for quantification theory, Journalof ACM, Volume 7 Issue 3 July 1960, Seiten 201-215.

97

Page 98: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

[DPLL62] Davis, M., Logemann, G., Loveland, D. (1962), A machine program for theorem pro-ving, Communications of the ACM, Volume 5 Issue 7 July 1962, Seiten 394-397.

[DIN05] Dinur, I., Regev, O., Smyth, C. (2005), The Hardness of 3-Uniform Hypergraph Colo-ring, Combinatorica, Volume 25 Issue 5 September 2005, Seiten 519-535.

[ERD60] Erdos, P., Rényi, A. (1960), On the evolution of random graphs, Publications of theMathematical Institute of the Hungarian Academy of Sciences 5, Seiten 17-61.

[FEL68] Feller, W. (1968), An Introduction to Probability Theory and Its Applications, Wiley.

[GAB11] Gableske, O., Heule, M. J. H. (2011), EagleUP: Solving random 3-SAT using SLS withunit propagation, Theory and Applications of Satisfiability Testing, Volume 6695 of LectureNotes in Computer Science, Seiten 367-368.

[HAG02] Häggström, O. (2002), Finite Markov Chains and Algorithmic Applications, LondonMathematical Society Student Texts, Band 52, Cambridge University Press.

[HOOS05] Hoos, H. H., Stützle, T. (2005), Stochastic Local Search Foundations and Applicati-ons, Morgan Kaufmann Publishers, San Francisco, CA

[KAR72] Karp, R. M. (1972), Reducibility among combinatorial problems, Complexity of Com-puter Computations, The IBM Research Symposia Series, Springer, Seiten 85-103.

[KON14] Konev, B., Lisitsa, A. (2014), A SAT Attack on the Erdos Discrepancy Conjecture, Theo-ry and Applications of Satisfiability Testing SAT 2014, Volume 8561 of Lecture Notes inComputer Science, Seiten 219-226.

[KRU12] Krumke, S. O., Noltemeier, H. (2012), Graphentheoretische Konzepte und Algorithmen,3. Auflage, Springer Vieweg.

[LI12] Li, C. M., Li, Y. (2012), Satisfying versus falsifying in local search for satisfiability, Pro-ceedings of SAT2012, Springer LNCS 7317, Seiten 477-478.

[MAT76] Matula, D. W. (1976), The largest clique size in a random graph, Technischer Report,Department of Computer Science, Southern Methodist University, Dallas.

[MUL02] Mulet, R., Pagnani, A., Weigt, M., Zecchina, R. (2002), Coloring random graphs, Phy-sical review letters 89, 268701, APS.

[ROT08] Rothe, J. (2008), Komplexitätstheorie und Kryptogie, eXamen.press, Springer.

[ROU11] Roussel O., (2011), Description of ppfolio, SAT Competition 2011, http://www.cril.univ-artois.fr/~roussel/ppfolio/solver1.pdf

[SCH99] Schöning, U. (1999), A probabilistic algorithm for k-SAT and constraint satisfactionproblems, Proc. 40th Sympos. on Fundations of Computer Science, FOCS 1999, IEEE, Sei-ten 410-414.

[SCH10] Schöning, U. (2010), Das SAT-Problem: die Drosophila der Komplexitätstheorie, Infor-matik Spektrum 33(5), Seiten 479-483.

[SCH12] Schöning, U., Torán, J. (2012), Das Erfüllbarkeitsproblem SAT, Mathematik für An-wendungen, Lehmann.

98

Page 99: New Schwere Instanzen für NP-schwere Probleme Hard instances … · 2018. 6. 11. · [COR09], Graphentheoretische Konzepte und Algorithmen von Sven Oliver Krumke [KRU12] und Hartmut

[SEL92] Selman, B., Levesque, H., Mitchell, D. (1992), A new method for solving hard satis-fiability problems, Proceedings of the Tenth National Conference on Artificial Intelligence(AAAI-92), San Jose, CA, Seiten 440-446.

[SON12] Sonobe, T., Inaba, M. (2012), Counter implication restart for parallel SAT solvers, LI-ON12 Proceedings of the 6th international conference on Learning and Intelligent Optimi-zation, Seiten 485-490, Springer.

[WEI07] Wei, W., Li, C. M., Zhang, H. (2007), Deterministic and random selection of variablesin local search for SAT, Solver description, SAT competition 2007.

[XU12] Xu, N., Zhu, J., Lu D., Zhou, X., Peng, X., Du, J. (2012), Quantum Factorization of 143on a Dipolar-Coupling Nuclear Magnetic Resonance System, Physical Review Letters 108

99