SAT 方法破解塔斯基高中代数问题：最小反例模型元素数及数量确定！

arXiv 平台介绍arXiv 平台提供搜索、提交、捐赠、登录等功能可按回车键进行搜索还有高级搜索选项。论文信息在数学的逻辑学领域有一篇 arXiv:2608.08421 的论文。该论文于 2026 年 8 月 9 日提交标题为“对塔斯基高中代数问题的 SAT 攻击”作者是贝尔纳多·苏贝卡索斯和本杰明·普日博茨基。可查看该论文的 PDF 版本、HTML实验性版本。塔斯基高中代数问题研究情况塔斯基的高中代数问题是关于正整数的加法、乘法和指数运算的每一个真等式是否都能从 11 条基本等式推导得出。威尔基证明了一个等式在正整数范围内成立但无法从塔斯基公理推导得出。古雷维奇给出了一个包含 59 个元素的代数结构它满足塔斯基公理但不满足威尔基等式。多年来多位作者不断缩小这种反例模型的规模最终由伯里斯和耶茨得到了一个包含 12 个元素的反例模型。另一方面张证明了不存在少于 11 个元素的反例模型。论文主要成果利用 SAT 方法论文作者证明了最小的反例模型包含 12 个元素正如伯里斯和耶茨所猜想的那样。此外还证明了在同构意义下包含 12 个元素的反例模型恰好有 8,957,952 个并对它们进行了简单的分类。该 SAT 方法在寻找等式理论反例模型方面优于专用工具 Mace4 和 SEM。而且通过自动形式化在 Lean 中证明了主要结果的正确性。论文其他信息论文有 21 页主题涉及逻辑学 (math.LO)、计算机科学中的逻辑学 (cs.LO)有相应的引用格式。提交历史显示来自贝尔纳多·阿尼瓦尔·苏贝卡索斯·罗阿于 2026 年 8 月 9 日星期日 02:32:31 UTC 提交文件大小 32 KB。全文链接及相关操作可查看论文的 PDF 版本、HTML实验性版本、TeX 源代码 还能查看许可。当前浏览上下文为 math.LO可进行上一篇、下一篇文章的切换也能查看最新文章、近期文章等。还可切换浏览方式如计算机科学 (cs)、计算机科学中的逻辑学 (cs.LO)、数学 (math) 等。此外还有参考文献与引用的相关内容可导出 BibTeX 引用。文献工具及相关项目文献工具包括文献与引用工具如文献浏览器、关联论文、文献地图、scite.ai 等、代码、数据与媒体相关工具如 alphaXiv、代码链接、DagsHub、GotitPub、Huggingface、ScienceCast 等、演示项目如 Replicate、Hugging Face Spaces、TXYZ.AI 等、推荐器与搜索工具如影响力花图链接、CORE 推荐器等。arXivLabs 介绍arXivLabs 是一个框架允许合作者直接在网站上开发和分享新的 arXiv 功能。与 arXivLabs 合作的个人和组织需认同并接受开放、社区、卓越和用户数据隐私价值观。若有能为 arXiv 社区增值的项目想法可了解更多关于 arXivLabs 的信息。