Apologies on the late response. The linked post has links to the SAT challenge. It is a great place to poke around. For books, I have liked A Gentle Introduction to Optimization (https://www.amazon.com/gp/product/1107658799) and Knuth's Art of Computer Programming V4 (https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat... or https://www.amazon.com/Art-Computer-Programming-Combinatoria...).

I'm not at all clear if there are good courses. Good luck diving on anything fun!

There has been big progress in automated theorem proving lately

https://en.wikipedia.org/wiki/Automated_theorem_proving

you just don't hear about it much because the technology is not so fashionable today. Also it is more clear what the limits are, I mean, Turing, Godel, Tarski and all of those apply to neural networks as well any other formal system but people mostly forget it.

Knuth wrote a really fun volume of The Art of Computer Programming about advances in SAT solvers which are the foundation for theorem provers

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.

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

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.