The best kittens, technology, and video games blog in the world.
Saturday, January 16, 2016
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.