Introduction to Mathematics of Satisfiability

Description

discovered on SAT Live

The book under review covers a number of topics related to the satisfiability problem of propositional logic formulas (SAT). Since Cook and Levin proved in the early 1970s the NP-completeness of SAT, this problem has been at the center of attention of computer science theoreticians as well as practitioners.
The book consists of 14 chapters. Chapters 1–6 are a more or less standard introduction to propositional logic: syntax and semantics (chapter 2), normal forms (chapter 3), the Craig interpolation theorem (chapter 4), the Post completeness theorem (chapter 5), and the proof of the compactness theorem based on König's lemma (chapter 6). Chapters 7–10 are devoted to clausal logic, i.e. to formulas in conjunctive normal form. In chapter 7 the resolution rule is presented and three completeness results are established: (i) for proofs based on resolution and subsumption rules, (ii) for resolution refutation proofs, and (iii) for the semantic resolution rule of Slagle. In chapter 8 four classical algorithms for testing satisfiability are considered: (i) the table method, (ii) tableaux, (ii) the Davis-Putnam algorithm, and (iv) the Davis-Putnam-Logemann-Loveland algorithm (DPLL). All of them work in exponential time. Some possible improvements of DPLL are discussed in brief. The main known subclasses of formulas for which SAT can be solved in polynomial time are presented in chapter 9. The algorithms for some of them (e.g., for positive formulas, negative formulas, and DNFs) are trivial. Developing polynomial algorithms for some other cases (e.g., Horn formulas, dual Horn formulas, and Krom formulas (2-CNFs)) requires special effort. The class of affine formulas (linear equations) can be solved using standard algebraic techniques. In chapter 10 it is shown how SAT can be embedded into integer programming and matrix algebra.
Chapter 11 includes the proof of the Cook-Levin theorem on the NP-completeness of SAT and 3-CNF. It is also shown that in most cases the satisfiability problem remains NP-complete for classes of formulas F decomposed into a union F1∪F2 so that F1 and F2 belong to different "easy'' classes from chapter 9. Chapters 12 and 13 illustrate some applications of SAT to knowledge representation. In the former it is shown how first-order formulas over finite domains and some special kinds of constraints can be reduced to SAT. In the latter, polynomial time equivalence is established between general constraint satisfaction over finite domains and SAT. Chapter 13 ends with a proof of the well-known Shaefer dichotomy theorem which divides classes of Boolean constraints into solvable in polynomial time and NP-complete. It seems that the last chapter, chapter 14, goes slightly beyond the main scope of the book. Stable models (answer set semantics) are considered for normal logic programs, and some applications of SAT solvers to their computation are discussed.
There are exercise sections attached to each chapter. The bibliography includes 48 references.
{Reviewer's remarks: The author's reference policy is unclear. The list of references is too short for the variety of material covered in the book. Most of the results are not attributed. Results that have author names associated with them are not accompanied by references to the original publications. For example, in Section 2.3 a special kind of partial valuation, autarky, is introduced without a reference to the work of B. Monien and E. Speckenmeyer [see Discrete Appl. Math. 10 (1985), no. 3, 287–295; MR0777220] where it was originally introduced. Then autarkies are investigated in Sections 7.7, 9.3, and 11.7, but there are no references to the papers of A. Van Gelder and of O. Kullmann which are the sources of most of the presented results.}

Reviewed by M. I. Dekhtyar

Although this area has a history of over 80 years, it was not until the creation of efficient SAT solvers in the mid-1990s that it became practically important, finding applications in electronic design automation, hardware and software verification, combinatorial optimization, and more. Exploring the theoretical and practical aspects of satisfiability, Introduction to Mathematics of Satisfiability focuses on the satisfiability of theories consisting of propositional logic formulas. It describes how SAT solvers and techniques are applied to problems in mathematics and computer science as well as important applications in computer engineering.

The book first deals with logic fundamentals, including the syntax of propositional logic, complete sets of functors, normal forms, the Craig lemma, and compactness. It then examines clauses, their proof theory and semantics, and basic complexity issues of propositional logic. The final chapters on knowledge representation cover finite runs of Turing machines and encodings into SAT. One of the pioneers of answer set programming, the author shows how constraint satisfaction systems can be worked out by satisfiability solvers and how answer set programming can be used for knowledge representation.

**