# Solving regex crosswords with Z3

DevFeed: [Solving regex crosswords with Z3](<https://devfeed.tech/articles/solving-regex-crosswords-with-z3-21962.md>)

Original publisher: [Read original article](<https://blog.nelhage.com/post/regex-crosswords-z3/>)

Author: Nelson Elhage

Published: 2025-10-21T14:00:00Z

Content type: tutorial

Language: en

Sources: [Nelson Elhage](<https://devfeed.tech/sources/nelson-elhage.md>)

Topics: [Regular expression](<https://devfeed.tech/topics/regular-expression.md>), [Automaton](<https://devfeed.tech/topics/automaton.md>), [Finite-state machine](<https://devfeed.tech/topics/finite-state-machine.md>), [Python](<https://devfeed.tech/topics/python.md>)

Tags: [code](<https://devfeed.tech/tags/code.md>), [dfa](<https://devfeed.tech/tags/dfa.md>), [experimentation](<https://devfeed.tech/tags/experimentation.md>), [performance](<https://devfeed.tech/tags/performance.md>), [python](<https://devfeed.tech/tags/python.md>), [regex](<https://devfeed.tech/tags/regex.md>)

## AI overview

This technical post explains how to solve regular-expression crossword puzzles with a Z3-backed solver. It describes encoding regular expressions as deterministic finite automata, using a Python library to convert regex syntax to finite-state machines, and exploring solver performance and implementation improvements.

## Source excerpt

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.