Last semester, at some point in my course on Data Structures and
Algorithms, once again I mentioned the SUDOKU problem. I am sure that
I haven’t covered all about it yet, and this post is just to remember
me about things that I would like to came back at some point:
In Common Lisp, some libraries make the problem so easy that is hard
to explain to the students why the logic based approaches are so
challenging. Examples are: computed-class, cells and screamer.
Sudoku as SAT is documented in the article  and we know that a
better encoding should be possible. I would love to continue the
experiments with SNARK theorem prover following ideas from the
papers  and .
T. Hillenbrand, D. Topic, and C. Weidenbach, “Sudokus as Logical
Puzzles”, pp. 1–11, Apr. 2016.
G. Santos-García and M. Palomino, “Solving Sudoku Puzzles with
Rewriting Rules”, pp. 1–16, 2006.
I. Lynce and J. Ouaknine, “Sudoku as a SAT Problem”, online.
So many interesting things to do!
Professor at EMAp/FGV, Researcher at IBM
arademaker AT gmail DOT com