sat-smt.codes Open in urlscan Pro
2a01:4f9:c010:aef3::1  Public Scan

Form analysis
0 forms found in the DOM

Text Content

SAT/SMT BY EXAMPLE

Written by Dennis Yurichev.

News: My Discord server/channels, twitter.

The PDF

The source code

Some history


STAY TUNED!

Subscribe to my news feed


AS SEEN ON...

... Hacker News, Reddit: 1, 2, 3.

... smt-lib mailing list.

... Goodreads


RECOMMENDED AT LEAST AT...

 * Brigham Young University (link, archived, screenshot);
 * Czech Technical University in Prague (link, screenshot);
 * Deggendorf Institute of Technology (link, screenshot);
 * IIT Dharwad (link, screenshot);
 * Indian Institute of Technology Guwahati (link, screenshot);
 * Johannes Kepler University Linz (screenshot);
 * Northeastern University (archived, screenshot);
 * Software and Computational Systems Lab (link, archived, screenshot);
 * Stanford #1 (link, archived, screenshot);
 * Stanford #2 (archived, screenshot);
 * University of California, Santa Cruz (link, archived, screenshot);
 * University of Kaiserslautern (link, screenshot);
 * University of Kiel (archived, screenshot);
 * University of Rochester (link, screenshot);
 * University of Science and Technology of China (link, archived, screenshot);
 * University of Toronto (link, archived, screenshot);
 * University of Waterloo (link, archived, screenshot);
 * Université de Sherbrooke (link, screenshot);
 * Univerzita Karlova (link, screenshot);
 * Utrecht University (link, screenshot);


PRAISE

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

--------------------------------------------------------------------------------