flâneur

Solving Regex Crosswords with Z3 - Made of Bugs

blog.nelhage.com · 4,444 words · saved by 1 readers

For a while now, I’ve been fascinated by Z3 and by SMT solving more broadly. While on pat leave recently, I was reminded of the existence of regular-expression crossword puzzles, and allowed myself to get nerdsniped by writing a Z3-backed solver. I expected to spend perhaps an afternoon cranking out a quick solver; I ended up getting sucked into understanding and debugging Z3 performance, and learning far more about Z3 and about SMT than I expected. In this post, I’ll describe my approach and my initial solver, and then dive into some of the improvements and variations I explored. All of my code is available on github, if you want to follow along or check out my final results. To briefly recap: A regular-expression crossword consists of a grid of (unknown) characters, which are to-be-determined. These characters are constrained by a set of given regular expressions, which must match a given row or column, once filled in. I chose to solve the regexle variant, specifically, which uses a

For a while now, I've been fascinated by Z3 and by SMT solving more broadly. While on pat leave recently, I was reminded of the existence of regular-expression crossword puzzles , and allowed myself to get nerdsniped by writing a Z3-backed solver. I expected to spend perhaps an afternoon cranking out a quick solver; I ended up getting sucked into understanding and debugging Z3 performance, and learning far more about Z3 and about SMT than I expected. In this post, I'll describe my approach and my initial solver, and then dive into some of the improvements and variations I explored. All of my c

saved by

related reading