Z3 Puzzle Solver Examples

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.