
Handbook of Satisfiability
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
More details
Other editions
Additional editions

Content
- Title page
- Contents
- Part I. Theory and Algorithms
- Chapter 1. A History of Satisfiability
- 1.1 Preface: the concept of satisfiability
- 1.2 The ancients
- 1.3 The medieval period
- 1.4 The renaissance
- 1.5 The first logic machine
- 1.6 Boolean algebra
- 1.7 Frege, logicism, and quantification logic
- 1.8 Russell and Whitehead
- 1.9 G"odel's incompleteness theorem
- 1.10 Effective process and recursive functions
- 1.11 Herbrand's theorem
- 1.12 Model theory and Satisfiability
- 1.13 Completeness of first-order logic
- 1.14 Application of logic to circuits
- 1.15 Resolution
- 1.16 The complexity or resolution
- 1.17 Refinement of Resolution-Based SAT Solvers
- 1.18 Upper bounds
- 1.19 Classes of easy expressions
- 1.20 Binary Decision Diagrams
- 1.21 Probabilistic analysis: SAT algorithms
- 1.22 Probabilistic analysis: thresholds
- 1.23 Stochastic Local Search
- 1.24 Maximum Satisfiability
- 1.25 Nonlinear formulations
- 1.26 Pseudo-Boolean Forms
- 1.27 Quantified Boolean formulas
- References
- Chapter 2. CNF Encodings
- 2.1 Introduction
- 2.2 Transformation to CNF
- 2.3 Case studies
- 2.4 Desirable properties of CNF encodings
- 2.5 Conclusion
- References
- Chapter 3. Complete Algorithms
- 3.1 Introduction
- 3.2 Technical Preliminaries
- 3.3 Satisfiability by Existential Quantification
- 3.4 Satisfiability by Inference Rules
- 3.5 Satisfiability by Search: The DPLL Algorithm
- 3.6 Satisfiability by Combining Search and Inference
- 3.7 Conclusions
- References
- Chapter 4. CDCL Solvers
- 4.1 Introduction
- 4.2 Notation
- 4.3 Organization of CDCL Solvers
- 4.4 Conflict Analysis
- 4.5 Modern CDCL Solvers
- 4.6 Bibliographical and Historical Notes
- References
- Chapter 5. Look-Ahead Based SAT Solvers
- 5.1 Introduction
- 5.2 General and Historical Overview
- 5.3 Heuristics
- 5.4 Additional Reasoning
- 5.5 Eager Data-Structures
- References
- Chapter 6. Incomplete Algorithms
- 6.1 Greedy Search and Focused Random Walk
- 6.2 Extensions of the Basic Local Search Method
- 6.3 Discrete Lagrangian Methods
- 6.4 The Phase Transition Phenomenon in Random k-SAT
- 6.5 A New Technique for Random k-SAT: Survey Propagation
- 6.6 Conclusion
- References
- Chapter 7. Fundaments of Branching Heuristics
- 7.1 Introduction
- 7.2 A general framework for branching algorithms
- 7.3 Branching tuples and the canonical projection
- 7.4 Estimating tree sizes
- 7.5 Axiomatising the canonical order on branching tuples
- 7.6 Alternative projections for restricted branching width
- 7.7 How to select distances and measures
- 7.8 Optimising distance functions
- 7.9 The order of branches
- 7.10 Beyond clause-sets
- 7.11 Conclusion and outlook
- References
- Chapter 8. Random Satisfiability
- 8.1 Introduction
- 8.2 The State of the Art
- 8.3 Random MAX k-SAT
- 8.4 Physical Predictions for Solution-space Geometry
- 8.5 The Role of the Second Moment Method
- 8.6 Generative models
- 8.7 Algorithms
- 8.8 Belief/Survey Propagation and the Algorithmic Barrier
- 8.9 Backtracking Algorithms
- 8.10 Exponential Running-Time for k & 3
- References
- Chapter 9. Exploiting Runtime Variation in Complete Solvers
- 9.1 Runtime Variation in Backtrack Search
- 9.2 Exploiting Runtime Variation: Randomization and Restarts
- 9.3 Conclusion
- References
- Chapter 10. Symmetry and Satisfiability
- 10.1 Motivating Example
- 10.2 Preliminaries
- 10.3 Group Theory Basics
- 10.4 CNF Symmetry
- 10.5 Automorphism Group of a Colored Graph
- 10.6 Symmetry Detection
- 10.7 Symmetry Breaking
- 10.8 Summary and a Look Forward
- 10.9 Bibliographic Notes
- References
- Chapter 11. Minimal Unsatisfiability and Autarkies
- 11.1 Introduction
- 11.2 Deficiency
- 11.3 Resolution and Homomorphism
- 11.4 Special Classes
- 11.5 Extension to non-clausal formulas
- 11.6 Minimal Falsity for QBF
- 11.7 Applications and Experimental Results
- 11.8 Generalising satisfying assignments through "autarkies
- 11.9 The autarky monoid
- 11.10 Finding and using autarkies
- 11.11 Autarky systems: Using weaker forms of autarkies
- 11.12 Connections to combinatorics
- 11.13 Generalisations and extensions of autarkies
- 11.14 Conclusion
- References
- Chapter 12. Worst-Case Upper Bounds
- 12.1 Preliminaries
- 12.2 Tractable and intractable classes
- 12.3 Upper bounds for k-SAT
- 12.4 Upper bounds for General SAT
- 12.5 How large is the exponent?
- 12.6 Summary table
- References
- Chapter 13. Fixed-Parameter Tractability
- 13.1 Introduction
- 13.2 Fixed-Parameter Algorithms
- 13.3 Parameterized SAT
- 13.4 Backdoor Sets
- 13.5 Treewidth
- 13.6 Matchings
- 13.7 Concluding Remarks
- References
- Part II. Applications and Extensions
- Chapter 14. Bounded Model Checking
- 14.1 Model Checking
- 14.2 Bounded Semantics
- 14.3 Propositional Encodings
- 14.4 Completeness
- 14.5 Induction
- 14.6 Interpolation
- 14.7 Completeness with Interpolation
- 14.8 Invariant Strengthening
- 14.9 Related Work
- 14.10 Conclusion
- References
- Chapter 15. Planning and SAT
- 15.1 Introduction
- 15.2 Notation
- 15.3 Sequential Plans
- 15.4 Parallel Plans
- 15.5 Finding a Satisfiable Formula
- 15.6 Improved SAT Solving for Planning
- 15.7 QBF and Planning with Nondeterministic Actions
- References
- Chapter 16. Software Verification
- 16.1 Programs use Bit-Vectors
- 16.2 Formal Models of Software
- 16.3 Turning Bit-Vector Arithmetic into CNF
- 16.4 Bounded Model Checking for Software
- 16.5 Predicate Abstraction using SAT
- 16.6 Conclusion
- References
- Chapter 17. Combinatorial Designs by SAT Solvers
- 17.1 Introduction
- 17.2 Quasigroup Problems
- 17.3 Ramsey and Van der Waerden Numbers
- 17.4 Covering Arrays
- 17.5 Steiner Systems
- 17.6 Mendelsohn Designs
- 17.7 Encoding Design Theory Problems
- 17.8 Conclusions and Open Problems
- References
- Chapter 18. Connections to Statistical Physics
- 18.1 Introduction
- 18.2 Phase Transitions: Basic Concepts and Illustration
- 18.3 Phase transitions in random CSPs
- 18.4 Local search algorithms
- 18.5 Decimation based algorithms
- 18.6 Conclusion
- References
- Chapter 19. MaxSAT
- 19.1 Introduction
- 19.2 Preliminaries
- 19.3 Branch and Bound Algorithms
- 19.4 Complete Inference in MaxSAT
- 19.5 Approximation Algorithms
- 19.6 Partial MaxSAT and Soft Constraints
- 19.7 Evaluations of MaxSAT Solvers
- 19.8 Conclusions
- References
- Chapter 20. Model Counting
- 20.1 Computational Complexity of Model Counting
- 20.2 Exact Model Counting
- 20.3 Approximate Model Counting
- 20.4 Conclusion
- References
- Chapter 21. Non-Clausal SAT and ATPG
- 21.1 Introduction
- 21.2 Basic Definitions
- 21.3 Satisfiability Checking for Boolean Circuits
- 21.4 Automatic Test Pattern Generation
- 21.5 Conclusions
- References
- Chapter 22. Pseudo-Boolean and Cardinality Constraints
- 22.1 Introduction
- 22.2 Basic Definitions
- 22.3 Decision Problem versus Optimization Problem
- 22.4 Expressive Power of Cardinality and Pseudo-Boolean Constraints
- 22.5 Inference Rules
- 22.6 Current Algorithms
- 22.7 Conclusion
- References
- Chapter 23. QBF Theory
- 23.1 Introduction
- 23.2 Syntax and Semantics
- 23.3 Complexity Results
- 23.4 Models and Expressive power
- 23.5 Q-Resolution
- 23.6 Quantified Horn Formulas and Q2-CNF
- References
- Chapter 24. QBFs reasoning
- 24.1 Introduction
- 24.2 Quantified Boolean Logic
- 24.3 Applications of QBFs and QBF reasoning
- 24.4 QBF solvers
- 24.5 Other approaches, extensions and conclusions
- References
- Chapter 25. SAT Techniques for Modal and Description Logics
- 25.1 Introduction
- 25.2 Background
- 25.3 Basic Modal DPLL
- 25.4 Advanced Modal DPLL
- 25.5 The OBDD-based Approach
- 25.6 The Eager DPLL-based approach
- References
- Chapter 26. Satisfiability Modulo Theories
- 26.1 Introduction
- 26.2 Background
- 26.3 Eager Encodings to SAT
- 26.4 Integrating Theory Solvers into SAT Engines
- 26.5 Theory Solvers
- 26.6 Combining Theories
- 26.7 Extensions and Enhancements
- References
- Chapter 27. Stochastic Boolean Satisfiability
- 27.1 Introduction
- 27.2 Definitions and Notation
- 27.3 Complexity of SSAT and Related Problems
- 27.4 Applications
- 27.5 Analytical Results
- 27.6 Algorithms and Empirical Results
- 27.7 Stochastic Constraint Programming
- 27.8 Future Directions
- References
- Subject Index
- Cited Author Index
- Contributing Authors and Affiliations
System requirements
File format: PDF
Copy protection: Watermark-DRM (Digital Rights Management)
System requirements:
- Computer (Windows; MacOS X; Linux): Use the free software Adobe Reader, Adobe Digital Editions, or any other PDF viewer of your choice (see eBook Help).
- Tablet/Smartphone (Android; iOS): Install the free app Adobe Digital Editions or another reading app for eBooks, e.g., PocketBook (see eBook Help).
- E-reader: Bookeen, Kobo, Pocketbook, Sony, Tolino and many more (only limited: Kindle).
The file format PDF always displays a book page identically on any hardware. This makes PDF suitable for complex layouts such as those used in textbooks and reference books (images, tables, columns, footnotes). Unfortunately, on the small screens of e-readers or smartphones, PDFs are rather annoying, requiring too much scrolling.
This eBook uses Watermark-DRM, a „soft” copy protection. This means that there are no technical restrictions to prevent illegal distribution. However, there is a personalised watermark embedded in the eBook that can be used to identify the purchaser of the eBook in the event of misuse and to provide evidence for legal purposes.
For more information, see our eBook Help page.