  In this article we demonstrate how to solve a variety of problems and puzzles
using the built-in SAT solver of the computer algebra system Maple. Once the
problems have been encoded into Boolean logic, solutions can be found (or shown
to not exist) automatically, without the need to implement any search
algorithm. In particular, we describe how to solve the $n$-queens problem, how
to generate and solve Sudoku puzzles, how to solve logic puzzles like the
Einstein riddle, how to solve the 15-puzzle, how to solve the maximum clique
problem, and finding Graeco-Latin squares.
