Schöning / Torán Das Erfüllbarkeitsproblem SAT

Algorithmen und Analysen
1. Auflage 2012
ISBN: 978-3-86541-724-4
Verlag: Lehmanns Media
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Deutsch, Band 1, 181 Seiten

Reihe: Mathematik für Anwendungen

SAT (für satisfiability) ist der Name des bekanntesten NP-vollständigen Problems, des Erfüllbarkeitsproblems der Aussagenlogik. Gegeben ist hierbei eine Formel mit Boole’schen Variablen und Verknüpfungen und gesucht wird eine „Lösung“, also eine Wertezuweisung an die Variablen, so dass die Formel wahr wird.

Dieses algorithmische Problem ist Dreh- und Angelpunkt für alle NP-Vollständigkeitsnachweise und wurde schon als „Drosophila“ der Algorithmik bezeichnet. Für SAT werden seit einiger Zeit leistungsstarke Algorithmen entwickelt, die in der Lage sind, Formeln mit hunderten oder tausenden von Variablen zu lösen. Bei schwierigen Formeln mit nur wenigen Lösungen kommt dies der sprichwörtlichen Suche nach der Nadel im Heuhaufen gleich. Wie derartige Algorithmen arbeiten und wie die zugehörigen logischen Kalküle und heuristischen Suchmethoden eingesetzt werden, wird in diesem Buch – die erste deutschsprachige Veröffentlichung zum Thema – eingehend und fundiert erklärt.

Der Titel erscheint als Band 1 der Reihe
Mathematik für Anwendungen

Diese Textbuchreihe soll zeigen, dass Mathematik mehr ist als nur eine Zusammenstellung von Theoremen und Definitionen – tatsächlich eröffnet die Mathematik die Möglichkeit, anwendungsnah Probleme der realen Welt zu lösen. Gedacht als Grundlage für Vorlesungen und Seminare in den Ingenieurwissenschaften und der Informatik, zielt jeder Band darauf ab, ein bestimmtes Thema kompakt und didaktisch durchdacht zu erfassen und dabei den Balanceakt zwischen formal-korrekter und informal-verständlicher Darstellung zu vollbringen. Nicht nur Studierende, sondern auch Praktiker aus der Industrie sowie Lehrer und Schüler in mathematischen Fächern werden diese Reihe zu schätzen wissen.

Mathematics for Applications

This series of textbooks is designed to demonstrate how mathematics is more than just a collection of theorems and definitions – it is a powerful means to solve real-world problems! Intended for use in lecture courses and seminars in any field of engineering or computer science, each volume aims for a compact and didactically sound presentation of its subject matter, balancing the demands of formal correctness with the need for general accessibility. Not only students, but also those working in technical professions, teachers of high school mathematics and even their students should find these books valuable.

Autoren/Hrsg.

Schöning, Uwe

Torán, Jacobo

Inhaltsverzeichnis

1;Titel
;2
2;Vorwort;4
3;Inhaltsverzeichnis;5
4;Einleitung;7
5;1 Erste Definitionen und Ergebnisse;8
5.1;1.1 Boole’sche Formeln und Belegungen;8
5.2;1.2 Konjunktive Normalform und CSP;14
5.3;1.3 Tseitin-Codierung und serien-parallele Graphen;17
5.4;1.4 Beispiele für SAT-Codierungen;23
5.5;1.5 Autarke Belegungen;26
5.6;1.6 Craig-Interpolanten;27
5.7;1.7 Erfüllbarkeit durch Kombinatorik;29
6;2 Resolutionskalkül;35
6.1;2.1 Kalküle und NP versus co-NP;35
6.2;2.2 Widerlegungsvollständigkeit;37
6.3;2.3 Unit-Klauseln, Subsumption und pure Literale;43
6.4;2.4 Strategien und Restriktionen;45
6.5;2.5 Exponentielle untere Schranke für die Länge von Resolutionsbeweisen;52
7;3 Polynomial-lösbare Spezialfälle;62
7.1;3.1 2-KNF;62
7.2;3.2 Horn-Formeln;66
7.3;3.3 Renamable Horn-Formeln;68
7.4;3.4 Schaefer-Klassifikation;71
8;4 Backtracking und DPLL-Algorithmen;72
8.1;4.1 DPLL und heuristische Funktionen;74
8.2;4.2 Monien-Speckenmeyer-Algorithmus;76
8.3;4.3 Paturi-Pudlák-Zane-Algorithmus;79
8.4;4.4 DPLL in der Praxis;83
8.4.1;4.4.1 Klausellernen;84
8.4.2;4.4.2 Nicht-chronologisches Backtracking;86
9;5 Lokale Suche und Hamming-Kugeln;88
9.1;5.1 Deterministische lokale Suche;89
9.2;5.2 Zufällige Anfangsbelegung;92
9.3;5.3 Überdeckungscodes;94
9.4;5.4 Ein random walk-Algorithmus;97
9.5;5.5 Moser-Scheder-Algorithmus;101
9.6;5.6 GSAT, WalkSAT, Novelty;106
9.7;5.7 Harte Formeln für lokale Suche;108
10;6 Weitere SAT-Algorithmen;111
10.1;6.1 Ein Divide-and-Conquer-Algorithmus;111
10.2;6.2 Stålmarck-Algorithmus;114
10.3;6.3 SAT-Algorithmen mit OBDDs;118
10.4;6.4 Randomisiertes Runden und die Cross-Entropy-Methode;120
11;7 Zufällige Klauselmengen und physikalische Ansätze;123
11.1;7.1 Schwellenwert und Phasenübergang;123
11.2;7.2 Zufällige erfüllbare Formeln;127
11.3;7.3 Ising-Modell und physikalisch motivierte Algorithmen;129
12;8 Abschlussdiskussion;135
13;Anhang;139
13.1;Programmieren in Pseudo-Code;139
13.2;Graphen;141
13.3;Asymptotische Notation und Rekursionsgleichungen;143
13.4;Effiziente Algorithmen, P und NP;145
13.5;Probabilistische Algorithmen und die Klasse RP;149
13.6;Boole’sche Schaltkreise;151
13.7;SAT ist NP-vollständig;154
13.8;Binäre Entscheidungsgraphen (BDDs);157
13.9;Zufallsvariablen;160
13.10;Markov-Ketten;164
13.11;Abschätzungen mit Binomialkoeffizienten;166
14;Literatur;168
15;Index;178

Über Autor(innen)

Dr. Uwe Schöning und Dr. Jacobo Torán sind Professoren am Institut für Theoretische Informatik in der Fakultät für Ingenieurwissenschaften und Informatik der Universität Ulm.