对塔斯基高中代数问题的SAT攻击

# 针对塔斯基高中代数问题的SAT攻击
来源：https://arxiv.org/html/2608.08421
###### 摘要
塔斯基高中代数问题询问：关于正整数加法、乘法和幂运算的每个真实恒等式，是否都可由11个初等恒等式推导得出。令人惊讶的是，Wilkie证明了以下恒等式在正整数上成立，但无法从塔斯基公理推导得出：\(\(1\+x\)y\+\(1\+x\+x2\)y\)x⋅\(\(1\+x3\)x\+\(1\+x2\+x4\)x\)y=\\displaystyle\\left\(\(1\+x\)^\{y\}\+\(1\+x\+x^\{2\}\)^\{y\}\\right\)^\{x\}\\cdot\\left\(\(1\+x^\{3\}\)^\{x\}\+\(1\+x^\{2\}\+x^\{4\}\)^\{x\}\\right\)^\{y\}=\(\(1\+x\)x\+\(1\+x\+x2\)x\)y⋅\(\(1\+x3\)y\+\(1\+x2\+x4\)y\)x\.\\displaystyle\\left\(\(1\+x\)^\{x\}\+\(1\+x\+x^\{2\}\)^\{x\}\\right\)^\{y\}\\cdot\\left\(\(1\+x^\{3\}\)^\{y\}\+\(1\+x^\{2\}\+x^\{4\}\)^\{y\}\\right\)^\{x\}\.
Gurevič给出了一个满足塔斯基公理但不满足Wilkie恒等式的59元代数。多年来，多位研究者不断缩小此类反例模型的规模，最终Burris和Yeats得到了一个12元的反例模型。另一方面，Zhang证明了不存在元素数少于11个的反例模型。我们使用SAT方法证明了最小的反例模型大小为12，验证了Burris和Yeats的猜想。此外，我们证明了在同构意义下恰好存在8,957,952个12元的反例模型，并提供了简单的分类方法。我们的SAT方法在寻找等式理论反例模型方面优于专用工具（如Mace4和SEM）。同时，通过自动化形式化，我们在Lean中证明了主要结果的正确性。

## 1 引言
*高中恒等式*是指以下11个熟悉的、涉及加法、乘法和幂运算的恒等式，它们在正整数上普遍成立：
x\+y\\displaystyle x\+y=y\+x\\displaystyle=y\+x\(HSI 1\)
\(x\+y\)\+z\\displaystyle\(x\+y\)\+z=x\+\(y\+z\)\\displaystyle=x\+\(y\+z\)\(HSI 2\)
x⋅1\\displaystyle x\\cdot 1=x\\displaystyle=x\(HSI 3\)
x⋅y\\displaystyle x\\cdot y=y⋅x\\displaystyle=y\\cdot x\(HSI 4\)
\(x⋅y\)⋅z\\displaystyle\(x\\cdot y\)\\cdot z=x⋅\(y⋅z\)\\displaystyle=x\\cdot\(y\\cdot z\)\(HSI 5\)
x⋅\(y\+z\)\\displaystyle x\\cdot\(y\+z\)=x⋅y\+x⋅z\\displaystyle=x\\cdot y\+x\\cdot z\(HSI 6\)
1x\\displaystyle 1^\{x\}=1\\displaystyle=1\(HSI 7\)
x1\\displaystyle x^\{1\}=x\\displaystyle=x\(HSI 8\)
xy\+z\\displaystyle x^\{y\+z\}=xy⋅xz\\displaystyle=x^\{y\}\\cdot x^\{z\}\(HSI 9\)
\(x⋅y\)z\\displaystyle\(x\\cdot y\)^\{z\}=xz⋅yz\\displaystyle=x^\{z\}\\cdot y^\{z\}\(HSI 10\)
\(xy\)z\\displaystyle\(x^\{y\}\)^\{z\}=xy⋅z\\displaystyle=x^\{y\\cdot z\}\(HSI 11\)
这些是*全部*的恒等式吗？更形式化地说，高中恒等式是否构成了\((Z\>0,\+,⋅,↑,1)\)(\\mathbb\{Z\}\_\{\>0\},\+,\\cdot,\\uparrow,1)的等式理论公理？
这个引人入胜的问题由Tarski在20世纪60年代提出，它激发了大量关于涉及幂运算恒等式的代数和分析问题的小型研究领域（例如参见\[24,17,16,8,4,1\]）。通过利用算术与类型论之间的类比，该主题还应用于检查带有积、箭头和和类型构造子的λ\\lambda-演算中的类型同构性\[13,12\]。
令人惊讶的是，1981年，Wilkie通过证明以下恒等式在\((Z\>0,\+,⋅,↑,1)\)(\\mathbb\{Z\}\_\{\>0\},\+,\\cdot,\\uparrow,1)中成立但不能由高中恒等式推导得出，对塔斯基问题给出了否定的回答\[32\]：
111Wilkie的论文直到2000年才发表。\(\(1\+x\)y\+\(1\+x\+x2\)y\)x⋅\(\(1\+x3\)x\+\(1\+x2\+x4\)x\)y=\\displaystyle\\left\(\(1\+x\)^\{y\}\+\(1\+x\+x^\{2\}\)^\{y\}\\right\)^\{x\}\\cdot\\left\(\(1\+x^\{3\}\)^\{x\}\+\(1\+x^\{2\}\+x^\{4\}\)^\{x\}\\right\)^\{y\}=\(\(1\+x\)x\+\(1\+x\+x2\)x\)y⋅\(\(1\+x3\)y\+\(1\+x2\+x4\)y\)x\.\\displaystyle\\left\(\(1\+x\)^\{x\}\+\(1\+x\+x^\{2\}\)^\{x\}\\right\)^\{y\}\\cdot\\left\(\(1\+x^\{3\}\)^\{y\}\+\(1\+x^\{2\}\+x^\{4\}\)^\{y\}\\right\)^\{x\}\.
Wilkie恒等式的合理性可通过观察1\+x3=\(1\+x\)⋅\(1−x\+x2\)(1\+x^\{3\}=\(1\+x\)\\cdot\(1\-x\+x^\{2\}\))以及1\+x2\+x4=\(1\+x\+x2\)⋅\(1−x\+x2\)(1\+x^\{2\}\+x^\{4\}=\(1\+x\+x^\{2\}\)\\cdot\(1\-x\+x^\{2\}\))来证明，因此其恒等式两边都等于\(\(1\+x\)y\+\(1\+x\+x2\)y\)x⋅\(\(1\+x\)x\+\(1\+x\+x2\)x\)y⋅\(1−x\+x2\)x⋅y\.\\left\(\(1\+x\)^\{y\}\+\(1\+x\+x^\{2\}\)^\{y\}\\right\)^\{x\}\\cdot\\left\(\(1\+x\)^\{x\}\+\(1\+x\+x^\{2\}\)^\{x\}\\right\)^\{y\}\\cdot\(1\-x\+x^\{2\}\)^\{x\\cdot y\}\.。但此推理无法用塔斯基公理进行，因为中间步骤包含子项1−x\+x2(1\-x\+x^\{2\})，而减法不属于我们的语言。Wilkie的独立性证明正是基于此类语法考量。
然而，通过构造塔斯基公理的有限模型（即*HSI代数*），其中Wilkie恒等式不成立，也可以证明其独立性。Gurevič\[15\]是首个构造此类反例模型的人。Gurevič的模型有59个元素，由此开启了确定使Wilkie恒等式不成立的最小HSI代数规模的探索。此历程记录于表1。
222其中部分结果未发表，且某些情况下作者未意识到早期更强的结果。该历史记录来自\[8\]，我们已更新以包含\[35\]和\[37\]。
表 1：Wilkie恒等式反例模型最小规模的界限历史
Burris和Yeats\[8\]猜想Wilkie恒等式的最小反例模型大小为12。使用基于SAT的方法，我们证实了他们的猜想：
###### 定理 1.1.
不存在元素数至多为11且使Wilkie恒等式不成立的HSI代数。
实际上，我们的方法允许我们分类所有12元反例模型：
###### 定理 1.2.
在同构意义下，恰好存在\(2^{12}\cdot 3^{7}=8,957,952\)个元素数为12且使Wilkie恒等式不成立的HSI代数。
如我们在第7节所示，这8,957,952个反例模型可通过给出一个简单的反例模型“模板”来简洁描述，其中少数参数可以独立变化。
1994年，Zhang\[36\]提出将上述问题作为模型搜索算法的挑战性基准。确实，使用模型搜索程序Mace4和SEM，Zhang\[37\]尽管投入数周计算时间，仍未能证明不存在11元素反例模型。获得上界同样具有挑战性：Burris和Yeats\[8\]需数月计算才找到其12元素反例模型。另一方面，使用我们的基于SAT方法，在个人计算机上约10分钟即可建立下界，约50分钟即可找到一个12元素反例模型。这与Zhang关于“SAT工具在此问题上不如其他问题有优势”的论断\[37\]相矛盾；我们将我们方法的成功归因于使用了打破对称性的约束和减少编码规模的辅助变量。
#### 相关工作。
在我们之前，SAT求解在寻找和枚举代数结构模型方面已有其他应用\[26,14,30,34\]。Meier和Sorge使用SAT及其他计算工具，根据有限代数结构满足的不同等式自动分类其同构类\[26\]。Gardam使用SAT找到了Kaplansky单位猜想的显式反例；有趣的是，Gardam工作中的代数结构是无限群环，但将SAT限制在该结构的有限部分足以找到反驳Kaplansky猜想的元素\[14\]。Zhang、Bonacina和Hsiang使用SAT解决了关于有限拟群的各类开放问题\[34\]。最近，Van Caudenberg、Bogaerts和Vendramin使用SAT枚举了杨-巴克斯特方程离散版本的非同构解\[30\]。

## 2 编码高中恒等式
考虑固定的n⩾1(n\\geqslant 1)。我们将描述如何编码具有n个元素的塔斯基公理模型，我们将其标识为集合Dn:=\{1 ̄,2 ̄,...,n ̄\}(D\_\{n\}:=\\\{\\overline\{1\},\\overline\{2\},\\dots,\\overline\{n\}\\\})。值得明确指出的是，这些是任意符号，因此例如，2 ̄⋅3 ̄=6 ̄(\\overline\{2\}\\cdot\\overline\{3\}=\\overline\{6\})并不必然成立。然而，我们假设1 ̄(\\overline\{1\})是常数符号1的指称。
我们首先引入变量Ai,j,k(\\mathsf\{A\}\_\{i,j,k\})表示i ̄\+j ̄=k ̄(\\overline\{i\}\+\\overline\{j\}=\\overline\{k\})，类似地，变量Mi,j,k(\\mathsf\{M\}\_\{i,j,k\})表示i ̄⋅j ̄=k ̄(\\overline\{i\}\\cdot\\overline\{j\}=\\overline\{k\})，变量Ei,j,k(\\mathsf\{E\}\_\{i,j,k\})表示i ̄j ̄=k ̄(\\overline\{i\}^\{\\overline\{j\}\}=\\overline\{k\})。我们通过仅对1⩽i⩽j⩽n(1\\leqslant i\\leqslant j\\leqslant n)和k∈\[n\](k\\in\[n\])引入Ai,j,k(\\mathsf\{A\}\_\{i,j,k\})和Mi,j,k(\\mathsf\{M\}\_\{i,j,k\})，隐式编码了加法和乘法的交换性。这样，Ai,j,k(\\mathsf\{A\}\_\{i,j,k\})同时表示i ̄\+j ̄=k ̄(\\overline\{i\}\+\\overline\{j\}=\\overline\{k\})和j ̄\+i ̄=k ̄(\\overline\{j\}\+\\overline\{i\}=\\overline\{k\})，M(\\mathsf\{M\})变量同理。相反，变量Ei,j,k(\\mathsf\{E\}\_\{i,j,k\})对所有i,j,k∈\[n\](i,j,k\\in\[n\])都存在。为简便起见，我们有时在i\>j(i\>j)下书写Ai,j,k(\\mathsf\{A\}\_\{i,j,k\})，按约定这指的是变量Aj,i,k(\\mathsf\{A\}\_\{j,i,k\})，对M(\\mathsf\{M\})变量也类似处理。
第一步，我们通过以下基数约束强制这些变量表示正确的二元运算：
∀i∈\[n\],∀j∈\{i,...,n\},\\displaystyle\\forall i\\in\[n\],\\forall j\\in\\\{i,\\dots,n\\\},∑k∈\[n\]Ai,j,k=1,\\displaystyle\\quad\\sum\_\{k\\in\[n\]\}\\mathsf\{A\}\_\{i,j,k\}=1,\(1\)
∀i∈\[n\],∀j∈\{i,...,n\},\\displaystyle\\forall i\\in\[n\],\\forall j\\in\\\{i,\\dots,n\\\},∑k∈\[n\]Mi,j,k=1,\\displaystyle\\quad\\sum\_\{k\\in\[n\]\}\\mathsf\{M\}\_\{i,j,k\}=1,\(2\)
∀i∈\[n\],∀j∈\[n\],\\displaystyle\\forall i\\in\[n\],\\forall j\\in\[n\],∑k∈\[n\]Ei,j,k=1\.\\displaystyle\\quad\\sum\_\{k\\in\[n\]\}\\mathsf\{E\}\_\{i,j,k\}=1\.\(3\)
我们直接编码这些约束：
333存在仅使用O(n)(O(n))子句的AtMostOne(\\mathsf\{AtMostOne\})约束编码\[23\]，但在此问题中我们未观察到其运行时优势，因此决定采用直接编码。
\(∑i=1nxi=1\)≡\(⋁i=1nxi\)∧AtMostOne⁡\(x1,...,xn\)≡\(⋁i=1nxi\)∧⋀i=1n⋀j=i\+1n\(xi ̄∨xj ̄\)\.\left\(\\sum\_\{i=1\}^\{n\}x\_\{i\}=1\\right\)\\equiv\\left\(\\bigvee\_\{i=1\}^\{n\}x\_\{i\}\\right\)\\land\\mathsf\{AtMostOne\}\(x\_\{1\},\\ldots,x\_\{n\}\)\\equiv\\left\(\\bigvee\_\{i=1\}^\{n\}x\_\{i\}\\right\)\\land\\bigwedge\_\{i=1\}^\{n}\\bigwedge\_\{j=i\+1\}^\{n}\(\\overline\{x\_\{i\}\}\\lor\\overline\{x\_\{j\}\}\)\.\(4\)
至此，我们已处理了HSI 1和HSI 4。接下来，恒等式HSI 3、HSI 7和HSI 8易于通过单元子句编码：
⋀i=1n\(Mi,1,i\),\\displaystyle\\bigwedge\_\{i=1\}^\{n\}\(\\mathsf\{M\}\_\{i,1,i\}\),\(5\)
⋀i=1n\(E1,i,1\),\\displaystyle\\bigwedge\_\{i=1\}^\{n\}\(\\mathsf\{E\}\_\{1,i,1\}\),\(6\)
⋀i=1n\(Ei,1,i\)\.\\displaystyle\\bigwedge\_\{i=1\}^\{n\}\(\\mathsf\{E\}\_\{i,1,i\}\)\.\(7\)
然后，我们关注HSI 2和HSI 5；由于它们同构，我们展示如何编码HSI 2，HSI 5的编码方式相同，只需将A(\\mathsf\{A\})变量替换为M(\\mathsf\{M\})变量。
对于HSI 2，让我们首先展示直接（但天真）的编码会是什么样子：
⋀i=1n⋀j=1n⋀k=1n⋀l=1n⋀m=1n⋀r=1n\(Ai,j,l∧Al,k,m∧Aj,k,r\)→Ai,r,m\.\bigwedge\_\{i=1\}^\{n\}\\bigwedge\_\{j=1\}^\{n\}\\bigwedge\_\{k=1\}^\{n\}\\bigwedge\_\{\\ell=1\}^\{n\}\\bigwedge\_\{m=1\}^\{n\}\\bigwedge\_\{r=1\}^\{n\}\\left\(\\mathsf\{A\}\_\{i,j,\\ell\}\\land\\mathsf\{A\}\_\{\\ell,k,m\}\\land\\mathsf\{A\}\_\{j,k,r\}\\right\)\\rightarrow\\mathsf\{A\}\_\{i,r,m\}\.
这种直接编码使用n^6(n^\{6\})个子句，源于必须对计算的所有中间结果进行分支：索引ℓ(\\ell)遍历i ̄\+j ̄(\\overline\{i\}\+\\overline\{j\})的所有可能结果，索引m(m)遍历\(i ̄\+j ̄\)\+k ̄((\\overline\{i\}\+\\overline\{j\})\+\\overline\{k\})的可能结果，r(r)遍历j ̄\+k ̄(\\overline\{j\}\+\\overline\{k\})的可能结果。
为避免子句数量激增，我们引入辅助变量来直观总结中间计算。具体地，令Ai,j,k,l2(\\mathsf\{A\}^\{2\}\_\{i,j,k,\\ell\})为一个变量，对应于\(i ̄\+j ̄\)\+k ̄=l ̄((\\overline\{i\}\+\\overline\{j\})\+\\overline\{k\}=\\overline\{\\ell\})*或*i ̄\+\(j ̄\+k ̄\)=l ̄(\\overline\{i\}\+\(\\overline\{j\}\+\\overline\{k\}\)=\\overline\{\\ell\})。因此，我们首先引入子句：
⋀i=1n⋀j=1n⋀k=1n⋀l=1n⋀m=1n\(\(Ai,j,m∧Am,k,l\)→Ai,j,k,l2\)∧\(\(Aj,k,m∧Ai,m,l\)→Ai,j,k,l2\),\\bigwedge\_\{i=1\}^\{n\}\\bigwedge\_\{j=1\}^\{n\}\\bigwedge\_\{k=1\}^\{n\}\\bigwedge\_\{\\ell=1\}^\{n\}\\bigwedge\_\{m=1\}^\{n\}\\left\(\(\\mathsf\{A\}\_\{i,j,m\}\\land\\mathsf\{A\}\_\{m,k,\\ell\}\)\\rightarrow\\mathsf\{A\}^\{2\}\_\{i,j,k,\\ell\}\\right\)\\land\\left\(\(\\mathsf\{A\}\_\{j,k,m\}\\land\\mathsf\{A\}\_\{i,m,\\ell\}\)\\rightarrow\\mathsf\{A\}^\{2\}\_\{i,j,k,\\ell\}\\right\),\(8\)
然后添加以下约束：
⋀i=1n⋀j=1n⋀k=1nAtMostOne⁡\(\{Ai,j,k,l2∣l∈\[n\]\}\)\.\bigwedge\_\{i=1\}^\{n\}\\bigwedge\_\{j=1\}^\{n\}\\bigwedge\_\{k=1\}^\{n\}\\mathsf\{AtMostOne\}\(\\\{\\mathsf\{A\}^\{2\}\_\{i,j,k,\\ell\}\\mid\\ell\\in\[n\]\\\}\)\.\(9\)
注意约束(8)和(9)仅产生O(n^5)(O(n^\{5\}))个子句。让我们立即展示如何验证至此的子句的正确性，特别是恒等式HSI 2，因为这将更一般地说明我们如何形式化地推理我们编码的正确性，其余恒等式的正确性论证几乎相同。
确实，令Φn(\\Phi\_\{n\})为至此构建的CNF公式（即子句(1)、(2)、(3)、(5)、(6)、(7)、(8)和(9)的合取）。让我们定义阶为n的L(\\mathcal\{L\})-*代数*S。