SAT/SMT by Example

Download PDF


Some history

As seen on Hacker News, Reddit: 1, 2, 3.

It's recommended at least in University of Toronto, Brigham Young University, Software and Computational Systems Lab, University of Kaiserslautern.


"This is quite instructive for students. I will point my students to this!" (Armin Biere).

""An excellent source of well-worked through and motivating examples of using Z3s python interface.'" (Nikolaj Bjorner, one of Z3's developers).

"Impressive collection of fun examples!" (Pascal Fontaine, one of veriT solver's developers.)

"This is a great book. I've been recommending it to the students in my SMT class, as it's (by far) the largest compendium of constraint satisfaction problems/solutions that I'm aware of, including tons of unique and obscure ones. Good work, Dennis!" (Rolf Rolles).

→ [back to the main page]