Schöning / Torán The Satisfiability Problem

Algorithms and Analyses
1. Auflage 2013
ISBN: 978-3-86541-648-3
Verlag: Lehmanns Media
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band 3, 178 Seiten

Reihe: Mathematik für Anwendungen

The satisfiability problem of propositional logic, SAT for short, is the first algorithmic problem that was shown to be NP-complete, and is the cornerstone of virtually all NP-completeness proofs. The SAT problem consists of deciding whether a given Boolean formula has a “solution”, in the sense of an assignment to the variables making the entire formula to evaluate to true.
Over the last few years very powerful algorithms have been devised being able to solve SAT problems with hundreds of thousands of variables. For difficult (or randomly generated) formulas these algorithms can be compared to the proverbial search for the needle in a haystack. This book explains how such algorithms work, for example, by exploiting the structure of the SAT problem with an appropriate logical calculus, like resolution. But also algorithms based on “physical” principles are considered.

Autoren/Hrsg.

Schöning, Uwe

Torán, Jacobo

Inhaltsverzeichnis

1;Preface;5
2;Title;3
3;Contents;6
4;Introduction;7
5;1 First Definitions and Results;9
5.1;1.1 Boolean Formulas and Assignments;9
5.2;1.2 Conjunctive Normal Form and CSP;14
5.3;1.3 Tseitin Encoding and Series-Parallel Graphs;18
5.4;1.4 Examples for Encoding into a SAT Problem;23
5.5;1.5 Autark Assignments;26
5.6;1.6 Craig Interpolants;27
5.7;1.7 Satisfiability by Combinatorics;29
6;2 Resolution Calculus;35
6.1;2.1 Calculi and NP versus co-NP;35
6.2;2.2 Refutation Completeness;36
6.3;2.3 Unit Clauses, Subsumption and Pure Literals;42
6.4;2.4 Strategies and Restrictions;44
6.5;2.5 Exponential Lower Bounds for the Length of ResolutionProofs;50
7;3 Special Cases Solvable in Polynomial Time;59
7.1;3.1 2-CNF;60
7.2;3.2 Horn Formulas;63
7.3;3.3 Renamable Horn Formulas;65
7.4;3.4 Schaefer Classification;67
8;4 Backtracking and DPLL Algorithms;69
8.1;4.1 DPLL and Heuristic Functions;71
8.2;4.2 Monien-Speckenmeyer Algorithm;73
8.3;4.3 Paturi-Pudl´ak-Zane Algorithm;76
8.4;4.4 DPLL in Practice;79
8.4.1;4.4.1 Clause Learning;80
8.4.2;4.4.2 Non-Chronological Backtracking;82
9;5 Local Search and Hamming Balls;83
9.1;5.1 Deterministic Local Search;84
9.2;5.2 Random Initial Assignments;86
9.3;5.3 Covering Codes;88
9.4;5.4 A RandomWalk Algorithm;91
9.5;5.5 Moser-Scheder-Algorithm;96
9.6;5.6 GSAT,WalkSAT, Novelty, ProbSAT;99
9.7;5.7 Hard Formulas for Local Search;102
10;6 More SAT Algorithms;106
10.1;6.1 A Divide and Conquer Algorithm;106
10.2;6.2 Stalmarck Algorithm;108
10.3;6.3 SAT Algorithms with OBDD’s;112
10.4;6.4 Randomized Rounding and the Cross-EntropyMethod;114
11.1;7.1 Threshold and Phase Transition;117
11.2;7.2 Random Satisfiable Formulas;121
11.3;7.3 Ising Model and Physically Motivated Algorithms;124
12;8 Heavy Tail Distributions and Restarts;129
13;9 Final Discussion;133
13.1;Appendix: Programming in Pseudo Code;137
13.2;Appendix: Graphs;139
13.3;Appendix: Asymptotic Notation and Recurrences;141
13.4;Appendix: Efficient Algorithms, P and NP;142
13.5;Appendix: Probabilistic Algorithms and the Class RP;146
13.6;Appendix: Boolean Circuits;149
13.7;Appendix: SAT is NP-complete;152
13.8;Appendix: Binary Decision Diagrams (BDD’s);155
13.9;Appendix: Random Variables;157
13.10;Appendix: Markov Chains;161
13.11;Appendix: Estimations with Binomial Coefficients;163
14;Index;175

Über Autor(innen)

The authors, Dr. Uwe Schöning and Dr. Jacobo Toran, are professors in the Institute of Theoretical Computer Science at the University of Ulm, Germany.