@raph successfully nerd-sniped me into writing a translator from Sudoku grids → Z3 programs.

Doing it in Scheme was a fun exercise: quasiquoting makes it easy to generate SMT-LIB syntax inline, and the whole program is only 27 lines!

Here's the code: https://github.com/mkeeter/sudoku-z3

#scheme