Browse Books

Reviewer: George Hacken

Satisfiability (SAT) solvers are algorithms that determine whether or not there exist assignments to Boolean variables such that conditions in those variables yield TRUE. These algorithms are now part of the program verification/software correctness enterprise [1]. This ten-chapter book, by experts in the field, demonstrates that problems "arising in such diverse fields as artificial intelligence, logic, graph theory, and linear algebra can be formulated as Boolean constraint satisfaction problems (CSP[s]).... [This book] is devoted to the study of the complexity of such problems." The book is a monograph, containing barely 100 pages of text, and is necessarily densely packed with theorems, lemmas, and proofs. A further characteristic of a monograph, which the book certainly possesses, is the enumeration, demonstration, and substantiation of specific results; the results here are the complexity measures that classify various Boolean CSPs. The authors have developed "a framework for classifying the complexity of Boolean CSP[s] in a uniform way," and have presented a taxonomy of such CSPs. The rules that the authors develop serve to classify "every [Boolean CSP] as ?easy' or ?hard.'" I don't know which mathematician said it first, but it seems that the more general a theorem is, the less deep it is (an uncertainty principle in its own right). So it is with complexity theory, which (to quote the authors) can be "so general that its results become too weak." This is the force behind the authors' focus on Boolean CSPs. The authors' monograph, an advanced distillation of their own and others' research, is aimed at researchers in complexity theory, optimization, or other discrete math areas. The introductory chapter sets forth the book's strategy, namely, to address "a restricted subclass [Boolean CSPs] of all [complexity] problems." (To get a bit ahead of ourselves, the word "restricted" should not discourage the prospective reader; the remainder of the book fairly bristles with powerful, pithy, and widely applicable results.) Complexity classes nondeterministic polynomial time (NP), polynomial space (PSPACE), sharp P (#P), maximization strict NP (MAX SNP), LOGSPACE, and Nick's class (NC) are introduced in chapter 2, along with the realization of the book's focus, namely, the definition of the Boolean-constraint versions of these complexity classes. Chapter 2 states the three types of CSPs: decision (Can the constraints be satisfied (yes or no)__?__), counting (In how many ways can they be satisfied__?__), and optimization (What are maximal or minimal variable-assignments that satisfy the constraints__?__) NP optimization (NPO), also introduced in chapter 2, is a class associated with optimization. Since this is an advanced book, no buildup is given to the models of computation that underlie the book; these are for the most part deterministic and nondeterministic Turing machines. The Kleene star is also used, under the assumption of the reader's tacit understanding. The definitions of the classes P and NP are nevertheless quite clear, and the statement that "intuitively ... the difference between P and NP is akin to the difference between efficiently finding a proof ... and efficiently verifying a proof" is very helpful. The definition of SAT follows development of the definitions of NP-hard and NP-complete. Parallel complexity, the class NC, is used to define P-hardness and P-completeness. Chapter 3 formally introduces Boolean constraint satisfaction problems. The authors formalize the distinction between constraints, functions, and their applications, and suggest that the reader parse the definition of constraint application carefully. The warning is well taken, as the latter definition (not repeated here) includes variables whose indices (subscripts) themselves have indices. This is not a criticism; it merely indicates the advanced nature of the book. Chapter 4 characterizes constraint functions. "[A]ll problems within a class ... fall into one of finitely many equivalence subclasses." SAT for a given family of constraint functions is either P or NP-complete (that is, there are two equivalence classes). The advanced level of the book is again revealed by the rapid-fire definitions: weakly positive/negative (Horn clauses); bijunctive; affine (and with width 2); 2-monotone; implicative hitting set, bounded; and C-closed. These definitions are used extensively and intricately in the material that follows. Chapter 5 introduces the authors' admittedly nonprecise notion of implementation: a collection of functions captures the behavior of a constraint by being implemented by that constraint. The central result is that large classes of constraint families implement a small number of functions. Chapter 6 uses these tools to show that any problem in a CSP class (decision, counting, one with quantifiers) is "either ¿easy' or at least as ¿hard' as any problem in [that] class." Chapters 7, 8, and 9 apply the developed theory to SAT, input-restricted CSPs, and the complexity of meta-problems. This last addresses the question, "What is the complexity of identifying tractable problems__?__" Though the immediate application of this excellent monograph may be the generation of more theory, it will reward you substantially, when you're ready for it. Online Computing Reviews Service