Part 1. Theory and Algorithms

Chapter 1. A History of Satisfiability
Chapter 2. CNF Encodings
Chapter 3. Complete Algorithms
Chapter 4. Conflict-Driven Clause Learning SAT Solvers
Chapter 5. Look-Ahead Based SAT Solvers
Chapter 6. Incomplete Algorithms
Chapter 7. Fundaments of Branching Heuristics
Chapter 8. Random Satisfiability
Chapter 9. Exploiting Runtime Variation in Complete Solvers
Chapter 10. Symmetry and Satisfiability
Chapter 11. Minimal Unsatisfiability and Autarkies
Chapter 12. Worst-Case Upper Bounds
Chapter 13. Fixed-Parameter Tractability

Part 2. Applications and Extensions

Chapter 14. Bounded Model Checking
Chapter 15. Planning and SAT
Chapter 16. Software verification
Chapter 17. Combinatorial Designs by SAT Solvers
Chapter 18. Connections to Statistical Physics
Chapter 19. MAX SAT, Hard and Soft Constraints
Chapter 20. Model Counting
Chapter 21. Non-clausal SAT and ATPG
Chapter 22. Pseudo-Boolean and Cardinality Constraints
Chapter 23. Theory of Quantified Boolean Formulas
Chapter 24. Reasoning with Quantified Boolean Formulas
Chapter 25. SAT Techniques for Modal and Description Logics
Chapter 26. Satisfiability Modulo Theories
Chapter 27. Stochastic Boolean Satisfiability