DIMACS: Series in Discrete Mathematics and Theoretical Computer Science 1997; 724 pp; hardcover Volume: 35 ISBN10: 0821804790 ISBN13: 9780821804797 List Price: US$191 Member Price: US$152.80 Order Code: DIMACS/35
 The satisfiability (SAT) problem is central in mathematical logic, computing theory, and many industrial applications. There has been a strong relationship between the theory, the algorithms, and the applications of the SAT problem. This book aims to bring together work by the best theorists, algorithmists, and practitioners working on the SAT problem and on industrial applications, as well as to enhance the interaction between the three research groups. The book features the application of theoretical/algorithmic results to practical problems and presents practical problems for theoretical/algorithmic study. Major topics covered in the book include practical and industrial SAT problems and benchmarks, significant case studies and applications of the SAT problem and SAT algorithms, new algorithms and improved techniques for satisfiability testing, specific data structures and implementation details of the SAT algorithms, and the theoretical study of the SAT problem and SAT algorithms. Features:  A comprehensive review of SAT research work over the past 25 years.
 The most recent research results.
 A spectrum of algorithmic issues and applications.
Copublished with the Center for Discrete Mathematics and Theoretical Computer Science beginning with Volume 8. Volumes 17 were copublished with the Association for Computer Machinery (ACM). Readership Graduate students and research mathematicians interested in computer science, mathematics, engineering, and operations research. Table of Contents  S. A. Cook and D. G. Mitchell  Finding hard instances of the satisfiability problem: A survey
 J. Gu, P. W. Purdom, J. Franco, and B. W. Wah  Algorithms for the satisfiability (SAT) problem: A survey
 P. W. Purdom and G. N. Haven  Backtracking and probing
 J. Franco  Relative size of certain polynomial time solvable subclasses of satisfiability
 M. V. Marathe, H. B. Hunt III, R. E. Stearns, and V. Radhakrishnan  Complexity of hierarchically and 1dimensional periodically specified problems. I: Hardness results
 O. Kullmann  Worstcase analysis, 3SAT decision, and lower bounds: Approaches for improved SAT algorithms
 K. Iwama and K. Takaki  Satisfiability of 3CNF formulas with small clause/variableratio
 D. A. Plaisted and G. D. Alexander  Propositional search efficiency and firstorder theorem proving
 J. Wang  Branching rules for propositional satisfiability test
 B. W. Wah and Y. Shang  A discrete Lagrangianbased globalsearch method for solving satisfiability problems
 M. G. C. Resende, L. S. Pitsoulis, and P. M. Pardalos  Approximate solution of weighted MAXSAT problems using GRASP
 J. Gu  Multispace search for satisfiability and NPhard problems
 S. Joy, J. Mitchell, and B. Borchers  A branch and cut algorithm for MAXSAT and weighted MAXSAT
 A. Løkketangen and F. Glover  Surrogate constraint analysisnew heuristics and learning schemes for satisfiability problems
 H. Kautz, B. Selman, and Y. Jiang  A general stochastic approach to solving problems with hard and soft constraints
 J. Hsiang and G. S. Huang  Some fundamental properties of Boolean ring normal forms
 S. K. Shukla, D. J. Rosenkrantz, H. B. Hunt, and R. E. Stearns  The polynomial time decidability of simulation relations for finite state processes: A HORNSAT based approach
 L. M. Kirousis, E. Kranakis, and D. Krizanc  A better upper bound for the unsatisfiability threshold
 R. Battiti and M. Protasi  Solving MAXSAT with nonoblivious functions and historybased heuristics
 E. Speckenmeyer, M. Böhm, and P. Heusch  On the imbalance of distributions of solutions of CNFformulas and its impact on satisfiability solvers
 H. van Maaren  On the use of second order derivatives for the satisfiability problem
 C. K. Rushforth and W. Wang  Local search for channel assignment in cellular mobile networks
 S. Areibi and A. Vannelli  A GRASP clustering technique for circuit partitioning
