ebook ebooks e-book e-books downloaden bei MyEbooks.ch downloaden

The Satisfiability Problem Algorithms and Analyses

:	Uwe Schöning, Jacobo Torán
:	The Satisfiability Problem Algorithms and Analyses
:	Lehmanns Media GmbH
:	9783865416483
:	1
:	CHF 8.90
:

:	Informatik, EDV
:	English

:	178
:	Wasserzeichen/DRM
:	PC/MAC/eReader/Tablet
:	PDF

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.

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.

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