作者用 AArch64 汇编为 macOS 写了一个约 200 行的数独求解器，完成了探索不同范式下的求解器系列——从 Agda 的正确性证明到原始汇编毫无安全网。代码直接利用 CPU 指令进行位运算操作（如 popcount 和候选掩码搜索），展示了在没有任何检查的情况下，汇编也能通过直接使用机器栈获得一些抽象。
背景
这是 Veit Heller 的"简单数独求解器"博客系列的一部分，探索不同范式下的约束求解——从证明助手到汇编语言。该系列此前已涵盖 Agda、Common Lisp 和 Forth。
- 来源
- Lobsters
- 发布时间
- 2026年10月26日 21:28
- 评分
- 5.0 / 10