本文通过SAT方法证明了Wilkie恒等式的最小反模型恰好有12个元素，确认了Burris和Yeats的猜想。作者枚举并分类了全部8,957,952个同构类反模型，结果优于Mace4和SEM等专用工具。
背景
塔斯基于1930年提出的初等代数问题：关于正整数加减乘幂的所有真恒等式是否都能从11条基本公理推导出来？Wilkie于1980年给出了反例，但最小反模型的构造问题悬而未决数十年。
- 来源
- Lobsters
- 发布时间
- 2026年8月31日 01:08
- 评分
- 8.0 / 10
本文通过SAT方法证明了Wilkie恒等式的最小反模型恰好有12个元素，确认了Burris和Yeats的猜想。作者枚举并分类了全部8,957,952个同构类反模型，结果优于Mace4和SEM等专用工具。
塔斯基于1930年提出的初等代数问题：关于正整数加减乘幂的所有真恒等式是否都能从11条基本公理推导出来？Wilkie于1980年给出了反例，但最小反模型的构造问题悬而未决数十年。