当"玩具项目"变成一场深潜——读《Solving regex crosswords with Z3》

当"玩具项目"变成一场深潜——读《Solving regex crosswords with Z3》

Nelson Elhage 在陪产假期间被一个正则表达式填字游戏"nerd-sniped"了。他本以为花一个下午就能写完一个求解器，结果一头扎进 Z3 的性能调优里，越陷越深。这篇文章记录了这段旅程，而它让我共鸣的，恰恰不是 Z3 的技术细节，而是一个程序员面对"明明应该很快却慢得离谱"时的那种执拗。

故事的开头很轻松：正则表达式描述的是正则语言，可以转成 DFA，把转移函数编码成 Z3 约束，然后让求解器去找满足所有线索的字符网格。思路清晰，代码也就几百行。拼起来一跑——3×3 的谜题要十分钟。作者凭直觉认为应该毫秒级就能解出来，于是不甘心，开始调试。

接下来的一系列优化构成了文章的主体，每一步都有清晰的因果：先用领域知识剪枝——从 DFA 里找出"死状态"和"死字符"，把显然不可能的选项提前排除，给 Z3 减负；再把转移函数从"未解释函数 + 逐点断言"改成显式的 if-then-else 表达式，促使 Z3 做等式推理而非回溯搜索；最后发现构造巨大表达式本身很慢，于是用 Z3 Lambda 或 macro-finder 战术让表达式只构造一次、多处复用。每一步都合理，但合在一起的效果是近百倍的加速。

真正让我印象深刻的是那些"说不通"的部分。作者无意中把状态变量的上界从一个线索的状态数改成了所有线索的最大状态数——一个更松的约束——结果快了十倍。他坦承自己完全不理解为什么。他还试了 Z3 原生的正则表达式理论，代码最简单，速度也不错，几乎比最初的朴素实现快十倍。这些经历指向一个他反复强调的结论：Z3 的性能"notoriously opaque and unstable"——不透明、不稳定，有时甚至违反直觉。

文章结尾的反思很诚实。他说这个项目本来只是个消遣，最终却花了不少时间重构、跑基准、画图，但他对 Z3 和 SMT-LIB 的理解因此深入了许多——而这本来就是他最初的目标。他还给了几条实用建议：如果 Z3 对你的问题领域有一等支持，先从那里开始；如果要用整数表示"N 选一"且没有算术语义，考虑用 EnumSort 避免莫名其妙的性能悬崖。

读完这篇文章，我最大的感触是：好的"玩具项目"从来不只是玩具。它是一个安全的沙盒，允许你把一个"应该很快"的直觉追到底，允许你在性能的迷宫里撞墙、回头、再换一条路。Elhage 没有在"能跑了"的时候停下，而是被"为什么这么慢"的好奇心拽着一路深挖，最终换来了对工具底层真正的理解。这种"因为不甘心所以学到东西"的路径，恐怕比任何系统教程都更扎实。