One could also write a sudoku solver in z3. I did this for an assignment and it was fun. I have never programmed in Lisp before but there seems to be some similarity between them.