Z3 Puzzle Solvers repository

Logic programming was once the next big thing, and like most next big things it fizzled. One useful thing which came out of it were constraint solvers, but because price of using them was writing Prolog, very few people bothered.

There was never any strong reason why constraint solver engines couldn't be used in other environments, and Z3 sort of does that - by working in Python 2.x. I'd obviously prefer if it supported Ruby, or at least Python 3, but it's still better than trying to remember how to parse strings in Prolog.

I played with Z3 a bit, wrote a bunch of puzzle solver scripts, and they're on github now. You probably won't need just another sudoku solver, but Z3 for Python has very few examples in its documentation, so this collection might actually be useful if you want to learn constraint solvers in some reasonable language.

Of course pull requests with more solvers or improvements to existing solvers most welcome.