数学 > 逻辑

[2026年8月9日提交]

标题：用SAT攻击塔斯基高中代数问题

作者：Bernardo Subercaseaux、Benjamin Przybocki

查看论文PDF（标题：用SAT攻击塔斯基高中代数问题），作者：Bernardo Subercaseaux和Benjamin Przybocki

摘要：塔斯基高中代数问题问的是：关于正整数加法、乘法和幂运算的每一个真恒等式，是否都可由11条初等恒等式推出？令人惊讶的是，Wilkie证明下面这个恒等式在正整数上成立，却不能由塔斯基公理推出：

((1+x)^y + (1+x+x^2)^y)^x * ((1+x^3)^x + (1+x^2+x^4)^x)^y = ((1+x)^x + (1+x+x^2)^x)^y * ((1+x^3)^y + (1+x^2+x^4)^y)^x.

Gurevič给出了一个包含59个元素的代数，它满足塔斯基公理但不满足Wilkie恒等式。多年来，多位研究者不断缩小此类反模型的大小，最终由Burris和Yeats得到大小为12的反模型。另一方面，Zhang证明了不存在小于11个元素的反模型。我们使用SAT证明了最小反模型的大小为12，正如Burris和Yeats所猜想的那样。此外，我们证明在同构意义下恰好存在8,957,952个12元素反模型，并给出了它们的简单分类。我们的SAT方法在寻找等式理论反模型方面优于专用工具Mace4和SEM。进一步地，我们使用自动形式化在Lean中证明了主要结果的正确性。

Comments：（无）

Subjects：Logic (math.LO); Logic in Computer Science (cs.LO)

引用为：arXiv:2608.08421 [math.LO]

（或 arXiv:2608.08421v1 [math.LO]）

https://doi.org/10.48550/arXiv.2608.08421

arXiv通过DataCite发布的DOI

提交历史

来自：Bernardo Anibal Subercaseaux Roa 查看邮箱

[v1] 2026年8月9日星期日 02:32:31 UTC（32 KB）

全文链接：

访问论文：

查看许可证

当前浏览上下文：

math.LO

下一页 | 新 | 最近 | 2026-08

切换浏览：

cs cs.LO math

参考文献与引用

BibTeX格式引用

书签

[BibSonomy](http://www.bibsonomy.org/BibtexHandler?requTask=upload&url=https://arxiv.org/abs/2608.08421&description=A SAT Attack on Tarski)
[Reddit](https://reddit.com/submit?url=https://arxiv.org/abs/2608.08421&title=A SAT Attack on Tarski)

文献与引用工具

代码、数据与媒体

演示

关于arXivLabs

arXivLabs是一个实验性项目框架，允许合作者直接在arXiv网站上开发和共享新功能。与arXivLabs合作的个人和组织都认同并接受了我们对开放性、社区、卓越和用户数据隐私的价值观。arXiv致力于这些价值观，只与遵守这些价值观的合作伙伴合作。

有可以为arXiv社区增值的项目想法吗？了解更多关于arXivLabs的信息。

本文作者中哪些人是背书人？ | 禁用MathJax（什么是MathJax？）