Number Hooks
A 9x9 grid puzzle: in each L-shaped hook of size k, place exactly k copies of digit k, with row and column sums fixed. Solved with Z3.
A constraint-satisfaction problem with three families of constraints (row sums, column sums, hook membership), solved directly with Z3 in a few lines of Python.