The regex-genex SMT constraint solver ( previously covered in https://news.ycombinator.com/item?id=2579783 ), as demonstrated by @LeventErkok ( https://gist.github.com/LeventErkok/4942496 ), is pretty good at solving this kind of puzzles. :-)