用 AArch64 汇编写一个两百行的数独求解器
来源：blog.veitheller.de — 2026-10-15
📋 概述
这是「简单数独求解器」系列第三季的第二篇，上一集用 Agda 写，求解器不给证明就不许交答案；这一集走到反面，用 macOS 上的 AArch64 汇编，什么都不检查。整个求解器两百多行：棋盘是 81 字节的扁平数组放在数据段，候选掩码继续用位运算，回溯直接用机器栈，popcount 和最低位查找都交给 CPU 指令而不是手写循环——在 Forth 那一集里需要自己实现的东西，这里硬件直接给你。
🔑 核心要点
- 选汇编的理由很干脆：在一切都由证明检查器的语言之后，看看 什么都不检查 时剩下什么
- 没有任何隐藏成本：没有分配器、没有 GC、没有运行时，棋盘被复制是因为我们写的指令就在复制它
- AArch64 的寄存器够用：31 个 64 位通用寄存器，小整数用 w 寄存器，参数走 x0 起，返回值回 x0
- 回溯不再自建棋盘栈——Forth 那集手搓的栈，这里就是 机器栈本身
- 位运算这一路一以贯之：候选掩码从 Common Lisp 那集用到现在，popcount 与最低位查找这次由 CPU 直接提供
- 没有类型系统之后，唯一挡在错误答案前面的只有写代码的人的谨慎
💡 金句
After a proof assistant that checks everything, it's worth looking at what's left when nothing is checked, and nothing is proven.
👍 0
👎 0
← 返回 Lobsters 首页