The article discusses the author's journey in creating a solver for regular-expression crosswords using the Z3 SMT solver. It details the process of encoding regular expressions as deterministic finite automata (DFAs) and integrating them into Z3 to solve the puzzles, along with insights gained during development. The author also shares their code on GitHub for others to explore.