Next semester, the Simons Institute will host a program on Fine-Grained Complexity and Algorithms Design, one of whose core topics is the exact complexity of satisfiability problems.

Coincidentally, Don Knuth has just posted online a draft of Section 7.2.2.2 of The Art of Computer Programming, which will be part of Volume 4B.
Chapter 7 deals with combinatorial searching; Section 7.2, titled “Generating all possibilities” is about enumeration and exhaustive search; Subsection 7.2.2 is about basic backtracking algorithms; and Sub-subsection 7.2.2.2 is about SAT.

Even people who are familiar with Don’s famously comprehensive approach to exposition might be surprised to see that this sub-subsection runs to 317 pages, 106 of which are devoted to solutions of exercises. Unfortunately, there was no space to provide the solution to Exercise 516.