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 220.127.116.11 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 18.104.22.168 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.