Sie sind hier
E-Book

Das Erfüllbarkeitsproblem SAT

Algorithmen und Analysen

AutorJacobo Torán, Uwe Schöning
VerlagLehmanns Media GmbH
Erscheinungsjahr2012
Seitenanzahl181 Seiten
ISBN9783865417244
FormatPDF
KopierschutzWasserzeichen/DRM
GerätePC/MAC/eReader/Tablet
Preis16,99 EUR
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.

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.

Kaufen Sie hier:

Horizontale Tabs

Blick ins Buch
Inhaltsverzeichnis
Titel
2
Vorwort4
Inhaltsverzeichnis5
Einleitung7
1 Erste Definitionen und Ergebnisse8
1.1 Boole’sche Formeln und Belegungen8
1.2 Konjunktive Normalform und CSP14
1.3 Tseitin-Codierung und serien-parallele Graphen17
1.4 Beispiele für SAT-Codierungen23
1.5 Autarke Belegungen26
1.6 Craig-Interpolanten27
1.7 Erfüllbarkeit durch Kombinatorik29
2 Resolutionskalkül35
2.1 Kalküle und NP versus co-NP35
2.2 Widerlegungsvollständigkeit37
2.3 Unit-Klauseln, Subsumption und pure Literale43
2.4 Strategien und Restriktionen45
2.5 Exponentielle untere Schranke für die Länge von Resolutionsbeweisen52
3 Polynomial-lösbare Spezialfälle62
3.1 2-KNF62
3.2 Horn-Formeln66
3.3 Renamable Horn-Formeln68
3.4 Schaefer-Klassifikation71
4 Backtracking und DPLL-Algorithmen72
4.1 DPLL und heuristische Funktionen74
4.2 Monien-Speckenmeyer-Algorithmus76
4.3 Paturi-Pudlák-Zane-Algorithmus79
4.4 DPLL in der Praxis83
4.4.1 Klausellernen84
4.4.2 Nicht-chronologisches Backtracking86
5 Lokale Suche und Hamming-Kugeln88
5.1 Deterministische lokale Suche89
5.2 Zufällige Anfangsbelegung92
5.3 Überdeckungscodes94
5.4 Ein random walk-Algorithmus97
5.5 Moser-Scheder-Algorithmus101
5.6 GSAT, WalkSAT, Novelty106
5.7 Harte Formeln für lokale Suche108
6 Weitere SAT-Algorithmen111
6.1 Ein Divide-and-Conquer-Algorithmus111
6.2 Stålmarck-Algorithmus114
6.3 SAT-Algorithmen mit OBDDs118
6.4 Randomisiertes Runden und die Cross-Entropy-Methode120
7 Zufällige Klauselmengen und physikalische Ansätze123
7.1 Schwellenwert und Phasenübergang123
7.2 Zufällige erfüllbare Formeln127
7.3 Ising-Modell und physikalisch motivierte Algorithmen129
8 Abschlussdiskussion135
Anhang139
Programmieren in Pseudo-Code139
Graphen141
Asymptotische Notation und Rekursionsgleichungen143
Effiziente Algorithmen, P und NP145
Probabilistische Algorithmen und die Klasse RP149
Boole’sche Schaltkreise151
SAT ist NP-vollständig154
Binäre Entscheidungsgraphen (BDDs)157
Zufallsvariablen160
Markov-Ketten164
Abschätzungen mit Binomialkoeffizienten166
Literatur168
Index178

Weitere E-Books zum Thema: Mathematik - Algorithmik - Arithmetik

Operations Research

E-Book Operations Research
Linearoptimierung Format: PDF

Linearoptimierung wird als mathematische Methode innerhalb des Operations Research bei der Mengenplanung für Absatz und Produktion sowie für Transport-, Netzfluss- oder Maschinenbelegungs-Probleme…

Operations Research

E-Book Operations Research
Linearoptimierung Format: PDF

Linearoptimierung wird als mathematische Methode innerhalb des Operations Research bei der Mengenplanung für Absatz und Produktion sowie für Transport-, Netzfluss- oder Maschinenbelegungs-Probleme…

Operations Research

E-Book Operations Research
Linearoptimierung Format: PDF

Linearoptimierung wird als mathematische Methode innerhalb des Operations Research bei der Mengenplanung für Absatz und Produktion sowie für Transport-, Netzfluss- oder Maschinenbelegungs-Probleme…

Gewöhnliche Differenzialgleichungen

E-Book Gewöhnliche Differenzialgleichungen
Differenzialgleichungen in Theorie und Praxis Format: PDF

Im Anschluss an Vorlesungen in Analysis und Linearer Algebra folgen an nahezu allen technischen und wirtschaftswissenschaftlich orientierten Studiengängen an Hochschulen und Universitäten als eine…

Mathematik für Informatiker

E-Book Mathematik für Informatiker
Format: PDF

Die Informatik entwickelt sich in einer unglaublichen Geschwindigkeit. Häufig ist die Mathematik Grundlage von Neuerungen. Deshalb ist sie unverzichtbares Werkzeug jedes Informatikers und Pflichtfach…

Mathematik für Informatiker

E-Book Mathematik für Informatiker
Format: PDF

Die Informatik entwickelt sich in einer unglaublichen Geschwindigkeit. Häufig ist die Mathematik Grundlage von Neuerungen. Deshalb ist sie unverzichtbares Werkzeug jedes Informatikers und Pflichtfach…

Mathematik für Informatiker

E-Book Mathematik für Informatiker
Format: PDF

Die Informatik entwickelt sich in einer unglaublichen Geschwindigkeit. Häufig ist die Mathematik Grundlage von Neuerungen. Deshalb ist sie unverzichtbares Werkzeug jedes Informatikers und Pflichtfach…

Weitere Zeitschriften

Berufsstart Bewerbung

Berufsstart Bewerbung

»Berufsstart Bewerbung« erscheint jährlich zum Wintersemester im November mit einer Auflage von 50.000 Exemplaren und ermöglicht Unternehmen sich bei Studenten und Absolventen mit einer ...

Bibel für heute

Bibel für heute

BIBEL FÜR HEUTE ist die Bibellese für alle, die die tägliche Routine durchbrechen wollen: Um sich intensiver mit einem Bibeltext zu beschäftigen. Um beim Bibel lesen Einblicke in Gottes ...

BIELEFELD GEHT AUS

BIELEFELD GEHT AUS

Freizeit- und Gastronomieführer mit umfangreichem Serviceteil, mehr als 700 Tipps und Adressen für Tag- und Nachtschwärmer Bielefeld genießen Westfälisch und weltoffen – das zeichnet nicht ...

Der Steuerzahler

Der Steuerzahler

Der Steuerzahler ist das monatliche Wirtschafts- und Mitgliedermagazin des Bundes der Steuerzahler und erreicht mit fast 230.000 Abonnenten einen weitesten Leserkreis von 1 ...

Deutsche Hockey Zeitung

Deutsche Hockey Zeitung

Informiert über das nationale und internationale Hockey. Die Deutsche Hockeyzeitung ist Ihr kompetenter Partner für Ihren Auftritt im Hockeymarkt. Sie ist die einzige bundesweite Hockeyzeitung ...

DULV info

DULV info

UL-Technik, UL-Flugbetrieb, Luftrecht, Reiseberichte, Verbandsinte. Der Deutsche Ultraleichtflugverband e. V. - oder kurz DULV - wurde 1982 von ein paar Enthusiasten gegründet. Wegen der hohen ...

F- 40

F- 40

Die Flugzeuge der Bundeswehr, Die F-40 Reihe behandelt das eingesetzte Fluggerät der Bundeswehr seit dem Aufbau von Luftwaffe, Heer und Marine. Jede Ausgabe befasst sich mit der genaue Entwicklungs- ...