This 310-page book is devoted to the topic of satisfiability. It is organized in a single chapter covering chapter 7.2.2.2 of the series. The book is essentially devoted to SAT solvers, and as we have come to expect from Knuth, will undoubtedly become the classic text on the topic through its elegant, precise, and thorough coverage. The reader needs to read the book from the beginning, as Knuth introduces the shorthand notation that he utilizes throughout the remainder of the text. Knuth begins by motivating the value of SAT solvers and introducing a few simple examples to make the reader comfortable. As problems are introduced, Knuth introduces algorithms to solve the problems and provides detailed, insightful explanations to accompany them. Conway’s Game of Life is even introduced as an example of bounded model checking.

This is not a light book. It takes time to read and digest the content, but the reader is assured of learning something on almost every page. Knuth ends his discussion on page 133 and then provides readers with a set of 526 problems (52 pages) to challenge them--and challenged you will be. The problems are varied and difficult, but Knuth provides answers to each of them over the course of the next 126 pages. Given this structure, the book is essentially one-third discussion and coverage of the topic and two-thirds devoted to interesting problems and demonstrating the value and power of the approaches covered.

More reviews about this item: Amazon