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