Archive for December, 2017

Z3 Puzzle Solver Examples

Sunday, December 17th, 2017


The one thing I enjoy more than solving logic problems is writing computer programs to solve logic problems.

Microsoft’s Z3 Theorem Prover is a very handy tool for doing this.

You can find my collection of example puzzle solvers here.

So far it includes solvers for Border Sum Sudoku, Chain Link Sudoku, Futoshiki, Mosaic, Stars, Suguru and Sujiko.