Solving Regex Crosswords with Z3 (blog.nelhage.com)

The author built a Z3-backed solver for regular-expression crosswords (specifically the hexagonal "regexle" variant), converting each clue’s regex into a deterministic finite automaton (using qntm’s greenery), flattening that DFA into a numpy transition table over an A–Z alphabet, and encoding grid characters and DFA states as Z3 integers. Matching a clue is expressed by asserting the DFA transition chain (state_0 = 0; state_{i+1} = T(state_i, char_i)) and that the final state is accepting. The implementation uses z3.Functions (and IntVector state arrays) to nail down transition behavior pointwise and wires those per-clue constraints into a global solver over the puzzle grid; code is available on GitHub. The project exposed the messy reality of SMT performance: initial solves for small puzzles could take minutes. Two practical fixes yielded the largest gains. First, domain-aware pruning: compute "dead" DFA states and dead vocabulary (via numpy analysis) and assert that grid characters and states cannot take those values, letting Z3 avoid large infeasible regions. Second, replace uninterpreted z3.Function transition encodings with explicit piecewise expressions for transitions (e.g., nested if-then-else), which lets the solver reason equationally instead of relying on search. (Enabling multiple cores gave only a small constant speedup.) The result is a fast, reliable hybrid approach that illustrates how light-weight domain analysis plus careful encoding can dramatically improve SMT-based solving for combinatorial string problems.