\myheading{et cetera}

Many puzzles from Martin Gardner's books can be solved effortlessly using SAT/SMT.
And it is such a fun, because SAT/SMT solvers can help understanding all the math theory behind them.

\myhrule{}

Also recommended by Armin Biere:

\begin{itemize}
\item Stuart Russell and Peter Norvig -- Artificial Intelligence: A Modern Approach

\item Helmut Veith, Edmund M. Clarke, Thomas A. Henzinger -- Handbook of Model Checking

\item Christos Papadimitriou -- Computational Complexity (1994)
\end{itemize}