Preface. n1. Heuristic-Based Backtracking Relaxation for Propositional Satisfiability; Bhalla et al. n2. Symbolic Techniques in Satisfiability Solving; Pan and Vardi.n3. Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas; Alekhnovich et al. n4. Backdoor Sets for DLL Subsolvers; S. Szeider. n5. The Complexity of Pure Literal Elimination; Johannsen.n6. Clause Weighting Local Search for SAT; Thornton.n7. Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings; Frisch et al. n8. Regular random k-SAT: properties of balanced formulas; Interian and Selman. n9. Applying SAT Solving for Classification in Finite Algebra; Meier and Sorge.n10. The SAT-Based Approch to Separation Logic; Armando et al.n11. MathSAT: Tight Integration of SAT and Mathematical Decision Procedures; Bozzano et al.
This book covers recent progress in solving propositional satisfiability and related problems. Propositional satisfiability is a powerful and general formalism used to solve a wide range of important problems including hardware and software verification. Research into methods to automate such reasoning has therefore a long history in artificial intelligence. This book follows on from the highly successful volume entitled SAT 2000 published five years ago.
Presents an up to date snapshot of a very active research area
Provides many practical applications (especially in the area of hardware verification)
Presents a survey of the breadth of research in this area