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