The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability

There has been big progress in automated theorem proving lately

https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat...

Everybody is aware that neural network techniques have improved drastically in performance, it's much more obscure that the toolbox of symbolic A.I. has improved greatly. Back in the 1980s production rules engines struggled to handle 10,000 rules, now Drools can handle 1,000,000+ rules with no problems.

Donald Knuth recently released the latest chapter of 'The Art of Computer Programming' and decided to tackle the topic of Satisfiability & SAT solvers ( @ https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat... ). Although he refers to algorithms in an vague way (using words like "Algorithm A" or "Algorithm J") and makes a determined effort to convey all information in the most mathematically precise way possible, I'm of the view that it's the finest work of it's kind on this topic. Having a section on something like 'random restarts' is great, but if you are already deep enough to have an interest in a paper like this, you are deep enough to learn about Luby sequences.

Vol 4A was published in 2011: https://www.amazon.com/Art-Computer-Programming-Combinatoria...

Vol 4B was partially published in fascicles: https://www.amazon.com/Art-Computer-Programming-Fascicle-Pre... and https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat...

Instead of the ultimate edition of vols 1-3, so far we've got a "patch" by Martin Ruckert who coordinated the volunteers: https://www.amazon.com/MMIX-Supplement-Computer-Programming-...