Lecture Notes

Some courses that are relevant to the topic:

• Advanced Topics in Logic: Automated Reasoning and Satisfiability, at Carnegie Mellon University. Lecture notes from the Fall 2024 iteration, taught by Marijn Heule.

Surveys or Overviews

• The Silent (R)evolution of SAT, by Johannes K. Fichte, Daniel Le Berre, Markus Hecher, and Stefan Szeider. CACM 2023.
• When Satisfiability Solving Meets Symbolic Computation, by Curtis Bright, Ilias Kotsireas, and Vijay Ganesh. CACM 2022.
• The Science of Brute Force, by Marijn Heule and Oliver Kullmann. CACM 2017.

Tutorials

A series of hands-on tutorials for SAT-solving towards combinatorial problems is available at https://bsubercaseaux.github.io/tutorials/. Those tutorials were co-authored by Bernardo Subercaseaux and Marijn Heule.

A book with plenty of examples, both for SAT and SMT solving, is available at https://smt.st/, thanks to Dennis Yurichev.

Workshops

• Simons + SLMath: AI For Math and TCS, April 2025.