💻 computer science

Witness-split + window-cardinality refinement for $r_3(N)$ : Architecture, empirical results, and a structural hard pocket

本文提出了一个结合了见证拆分（witness-splitting）、窗口基数剪枝（window-cardinality pruning）以及混合 SAT/MIP 求解器的可复现计算框架，用于严谨地研究 $r_3(212)$ 的上界，成功消除了大多数候选 44-集合，同时隔离了两个尽管经过大量验证工作仍未被证明的顽固结构案例。

原作者： Mehmet Ergezer

发布于 2026-06-04

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Mehmet Ergezer

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正试图往一个行李箱里（数字范围从 1 到 212）装尽可能多的物品，但必须遵守一个严格的规则：你不能挑选出三个构成完美算术级数模式的物品。

例如，如果你选择了数字 2，那么你就不能同时选择 4 和 6，因为 $2, 4, 6$ 是一个模式，其中每个数字都比前一个数大 2。这被称为“三项算术级数”。

数学家们一直在研究，在行李箱大小为 212 的情况下，你最多能装入多少件物品。对于大小为 211 的行李箱，已知答案是 43。而这篇论文的核心问题是：能否在大小为 212 的行李箱中装入 44 件物品？

作者 Mehmet Ergezer 不仅仅是在猜测；他构建了一个庞大的数字工厂，试图证明装入 44 件物品是不可能的。以下是这篇论文的拆解方式，使用了简单的类比：

1. 策略：“见证者拆分”工厂 (The "Witness Split" Factory)

尝试检查 212 个数中所有可能的 44 个数的组合，就像试图在地球上每一片沙滩上寻找一颗特定的沙粒一样。对于一台计算机来说，这太庞大了，无法单独处理。

因此，作者使用了一个聪明的技巧：

见证者 (The Witness)： 他从一个已知的、能够满足条件的 43 个数字的“安全列表”开始。
拆分 (The Split)： 他从这个安全列表中提取了 24 个最“重要”的数字，并要求计算机检查针对这些数字的所有可能的“是/否”场景。
结果： 这将这座不可逾越的数据大山分解成了 1250 万个较小的、可处理的“堆” (chunks)。然后，计算机尝试逐一解决每一个堆。

2. 工具：“窗口”与“精炼” (The "Window" and the "Refinement")

为了提高计算机的速度，作者添加了两个特殊的工具：

窗口卡 (The Window Card / 剪枝器)： 想象你正透过一扇窗户观察行李箱的一个小部分。我们已经从之前的数学研究中得知，一个大小为 50 的小窗口只能容纳（例如）10 个物品。计算机利用这一规则，可以立即剔除任何试图在该窗口内放入 11 个物品的“堆”。这是最强大的工具，它减少了近 30% 的困难堆。
精炼 (The Refinement / 深度挖掘)： 如果一个“堆”在 60 秒内难以解决，计算机并不会放弃。它会针对那个特定的困难“堆”，添加更多规则，并在更长的时间限制内再次尝试。这就像是面对一个锁着的盒子，通过挑选一把特定的锁，并用一把更大的钥匙再次尝试。

3. 结果：“硬核口袋” (The "Hard Pocket")

在超级计算机集群上运行了数百万次此类检查后，结果如下：

零成功： 计算机从未找到过任何一种有效的方法来装入 44 个数字。每当它尝试时，都会撞上一堵墙并表示：“不可能。”
证据： 这是证明 44 是不可能的有力证据，但它还不是一个正式的证明。为什么呢？因为仍然有一些顽固的“堆”计算机没能在规定时间内完成处理。

“硬核口袋” (The "Hard Pocket" / 具抗性的块)：
在数百万个“堆”中，作者发现了一个极其顽固的小组，共有 45 个“堆”，即使在给予额外时间和不同工具后，它们仍然无法被解决。

LP 攻击： 他们尝试了一种不同类型的数学求解器（称为 HiGHS），这种求解器将问题视为一条平滑的曲线。它未能解决这 45 个“堆”中的任何一个。
CDCL 攻击： 他们尝试了第三种求解器（称为 CDCL），这种求解器的工作方式像是一个侦探，能从错误中学习。这个求解器成功了！它解决了 45 个中的 18 个。
最后的 2 个： 然而，2 个“堆”（标记为 T1c）仍然完全无法解决。它们抵制了第一种求解器、第二种求解器以及第三种求解器。它们是这个问题的“最终 Boss”。

4. 结论：“单位间隙” (The "Unit Gap")

论文得出以下结论：

我们有一个验证过的、包含 43 个数字的有效列表。
我们有强有力的证据表明 44 是不可能的，因为计算机尝试了数百万次却失败了。
然而，由于那 2 个最后的顽固堆 的存在，我们目前还没有得到 100% 的数学证明。答案几乎可以肯定就是 43，但 43 与 44 之间的“间隙”在技术上仍然是开放的。

5. 给社区的礼物

作者并没有仅仅说“我放弃了”，而是释放了所有的相关数据。他将这 2 个顽固的“堆” 抛给了世界，作为一项挑战。

他提供了精确的代码和数据，以便其他数学家可以尝试只解决这两个“堆”。
他甚至将问题翻译成了一种用于形式化证明系统（Lean）的语言，邀请计算机科学家尝试使用逻辑引擎来进行证明。

简而言之： 作者构建了一台庞大的数字机器，试图打破不带模式地装填数字的记录。机器未能找到打破记录的方法，但它在两个微小且极其困难的谜题上卡住了。论文的含义是：“我们 99.9% 确定答案是 43，但这里有两个你需要解决的最终谜题，才能完成最终的证明。”

技术摘要：针对 $r_3(212)$ 的证人拆分与窗口基数细化研究

问题陈述
本文探讨了 $r_3(N)$ 的精确计算问题，其中 $r_3(N)$ 定义为包含不含非平凡三项等差数列（3-AP）的 $[1, N]$ 子集的最大规模。虽然渐近行为已有深入研究（例如 Roth 定理、Kelley–Meka），但本文的重点在于 $N=212$ 这一有限前沿。基于 OEIS A003002， $r_3(211) = 43$ 。作者研究的是如下决策问题：是否存在一个包含 44 个元素的 44-集，其构成 $[1, 212]$ 中的 3-AP 无集合？
作者已独立验证了一个 43 元素的证人（witness），确立了 $r_3(212) \ge 43$ 。上界问题的核心在于： $r_3(212)$ 是否 $\le 43$ 。任何假设的 44-集的一个必要条件是它必须包含端点 1 和 212；否则，它将可以平移为 $[1, 211]$ 中的 44-集，从而与已知数值矛盾。因此，问题简化为证明包含 $\{1, 212\}$ 的 44-集是不可能的。

方法论与架构
作者提出了一种结合五个组件的可复现计算框架，用于搜索可能的 44-集：

决策形式 CP-SAT 模型： 问题使用 $[1, 212]$ 范围内的布尔变量 $x_i$ 进行编码。约束包括：
- 3-AP 不等式：对于所有构成 AP 的三元组 $(a, b, c)$ ， $x_a + x_b + x_c \le 2$ 。
- 基数相等约束： $\sum x_i = 44$ （相比不等式，这在传播方面更紧凑）。
- 端点强制约束： $x_1 = x_{212} = 1$ 。
- 对称性破缺：通过字典序排列来消除反射对称性。
证人拆分（Witness-Splitting）： 为了管理搜索空间，作者使用了一个经过验证的 43 元素证人 $A_{43}$ 。他们根据元素的 AP 出现度（AP-incidence degree）对 $A_{43}$ 中的元素进行排序，并选取前 24 个。通过固定这 24 个变量的值，将搜索空间拆分为 $2^{24}$ 个“块”（chunks）。如果固定前缀强制产生了 3-AP，许多块会被立即剪枝。
窗口基数剪枝（Window-Cardinality Pruning）： 一项关键干预是添加了源自 OEIS A003002 的有效不等式。对于任何窗口 $[a, a+L-1]$ ，变量之和受 $r_3(L)$ 限制。对于 $N=212$ ，这增加了 22,154 个不等式，显著增强了模型，使其超越了原始的 3-AP 约束。
递归细化（Recursive Refinement）： 对于在宽层级（深度 24）返回 UNKNOWN 的块，通过使用下一个最高度数的证人变量扩展固定前缀来进行细化（深度分别为 40, 48, 56, 64），并使用更长的时限重新求解。
求解器多样性与工程化： 该任务利用基于 SLURM 的流水线在 UMass Unity 集群上运行。它采用了：
- CP-SAT (OR-Tools)： 用于宽层级扫描和递归细化。
- HiGHS (MIP)： 基于 LP 松弛的求解器，用于攻击最困难的 "UNKNOWN" 块。
- CDCL/SAT (CaDiCaL)： 用于重新攻击那些对 LP 方法具有抗性的块，并生成用于不可满足性证明的 DRAT 证明。

实证结果
该任务在深度-24 扫描及各种细化层级中处理了数百万个子问题。

零可行解： 在所有测试的子问题（宽层级扫描、细化、HiGHS 以及 CDCL）中，均未发现任何可行的 44-集。这为 $r_3(212) = 43$ 提供了强有力的经验支持，尽管这并非正式证明。
窗口基数的影响： 启用窗口基数不等式使宽层级扫描中的 UNKNOWN 率降低了约 28 个百分点（例如，在受控批次中从约 30% 降至约 1.65%），使其成为最有效的剪枝层。
结构性难题区（The Structural Hard Pocket）：
- 从一个 100,000 块的扩展批次中，有 6,071 个块返回 UNKNOWN。
- 对这些块进行 300 秒回收采样后，剩余 45 个具有抗性的块（T1 级）。
- HiGHS 攻击： 一次一小时的 HiGHS 运行关闭了 0/45 个块。一次 8 小时的审计关闭了 25/45 个块，留下 20 个块（T1b 级），其对偶界限被锁定在 0.0，表明 LP 松弛无法提供不可满足性的证明。
- CDCL 攻击： 对 20 个 T1b 块进行的纯 CDCL/SAT 攻击关闭了 18/20 个块，并生成了独立验证的 DRAT 证明。
- 残余部分（T1c）： 即使在 12 小时的纯 CDCL 运行和 4 小时的窗口化 CDCL 诊断之后，仍有两个块（ID 40959 和 48895）保持 UNKNOWN 状态。这两个块在 CP-SAT、HiGHS (LP-MIP) 和 CDCL 范式下均表现出抗性。

主要贡献
论文明确将其贡献界定为方法论层面，而非提出了 $r_3(212)$ 的新精确值。具体贡献如下：

架构： 一个结合了证人拆分、窗口基数剪枝和递归细化的可复现框架，用于精确上界搜索。
实证说明： 对 $N=212, K=44$ 任务的详细分析，包括求解器权衡以及搜索空间的不均匀性（例如，“由中向外”且具有特定分配特征的块明显更难）。
难题区表征： 识别出了一个在充足时间限制下对 CP-SAT、HiGHS 和 CDCL 范式均保持不变的结构性障碍（T1c）。
基准发布： 分层发布实例：
- T1a： 由 HiGHS 关闭的 25 个块。
- T1b \ T1c： 由 CDCL 结合 DRAT 证明关闭的 18 个块。
- T1c： 最终剩下的 2 个抗性块，被视为最尖锐的开放问题。
- T2/T3： 6,071 个宽层级 UNKNOWN 块以及用于未来尝试的完整 12.5M 块生成器。
形式化： 用于形式化证明搜索系统的 Lean 4 编码。

意义与主张
作者谦虚地声称，虽然该任务有力地支持了 $r_3(212) = 43$ 的猜想，但由于存在未解决的 T1c 残余，因此不能构成正式证明。其意义在于隔离了具体的计算障碍：

已认证界限之间的差距恰好为 1（ $43 \le r_3(212) \le 44$ ）。
LP 方法（HiGHS）的失败以及 CDCL 的部分成功表明，这种困难性不仅仅是传播伪影，而是一种结构性属性，其中 LP 松弛间隙非常紧密，且整数不可满足性证明在组合上是弥散的。
论文认为，要弥合这一差距，需要更强的加法组合学界限（例如，傅里叶分析或多窗口划分界限）或者能够利用未被通用求解器捕获的特定问题对称性的定制分支定界系统。

这项工作作为基准，为社区提供了特定的、经过验证的实例（T1c），这些实例代表了当前通用组合优化求解器处理此类问题的极限。