Unfortunately Z3 was not available for Ruby or even Python 3, so I decided to do some exercises to learn how to use Z3 with Python 2.x.

In other words - use Python 2.x to run these.

To get z3 library, run this or equivalent:

$ brew install z3

Unfortunately some solvers don't fully follow rules of puzzles they try to solve, if rules were rather difficult to implement.

Complete:

• bridges
• light up
• minisudoku
• nonogram: gets bad solution anyway, as example puzzle was ambiguous
• selfref
• sudoku
• verbal arithmetic

Incomplete:

• clogic: no three same rule missing, gets correct solution anyway
• letter connections: phantom loops possible; rarely problem in practice
• slitherlink: all connected rule missing
• trees: 1-1 tree-camp mapping missing

Broken:

• nurikabe: my approach is probably not going to work

After writing those I decided to write Ruby interface for Z3 as well. Currently it's in fairly experimental stage, so it's probably still better to use Python 2 for serious business.

Solvers in the repository have Ruby versions available at https://github.com/taw/z3/tree/master/examples