Lecture Notes

The following slides correspond to the Marktoberdorf summer school course taught by Marijn Heule in 2025.

• SAT4Math: Introduction and Solvers
• Abstraction & Discrete Geometry
• Proofs and Chromatic Number of the Plane
• Beyond NP and Collatz Conjecture

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.

Others

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.