SAT/SMT by Example

Written by Dennis Yurichev.

Target audience: CS/math geeks.

Attention! Achtung! The new domain is The old one (which is will be defunct in Sep-2024. Please update your bookmarks, as they say.

News: Demographics of SAT/SMT.

Download the PDF

The source code

Some history

Stay tuned!

Subscribe to my news feed, my Discord server/channels, twitter.

As seen on...

... Hacker News: 1, 2; Reddit: 1, 2, 3, 4;; twitter; smt-lib mailing list; Goodreads.

Recommended at least at...


"Dennis Yurichev's "SAT/SMT by Example" is an impressive monograph. It provides an extensive and diverse collection of problems that can be encoded as SAT or SMT problems, and discusses their encodings in detail. Its wealth of SMT examples in particular has made it popular among researchers and practitioners interested in leveraging the power of SMT solvers." ( Cesare Tinelli, one of CVC4's authors )

"This is quite instructive for students. I will point my students to this!" (Armin Biere, one of Boolector's authors).

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

What Martin Nyx Brain said (48:40-49:17)