SAT 破解 Tarski 高中代数难题

A SAT Attack on Tarski's High School Algebra Problem

Tarski 的高中代数问题曾困扰学界多年：正整数上的加、乘、幂运算恒等式是否都能由 11 条基础公理推导？Wilkie 发现了一个反例，而 Gurevič 随后给出了一个包含 59 个元素的代数模型来反驳。此后，Burris 和 Yeats 将反例模型缩小至 12 个元素，并猜想这是最小规模。本文利用 SAT 技术证实了这一猜想，证明 12 确实是反例模型的最小规模。研究不仅找到了全部 8,957,952 个非同构的 12 元素反例模型，还给出了它们的简单分类。此外，该 SAT 方法在性能上超越了 Mace4 和 SEM 等专用工具，并通过 autoformalization 在 Lean 中验证了核心结论的正确性。