从有限到无限：通过 SAT 对诺林猜想获得更精细的渐近界限

诺林 (2008) 猜想指出，对超立方体 $Q_n$ 的任意 $2$-色边着色若要求对偶边接收不同颜色，则必须包含至少一对对偶顶点之间的长度为 $n$ 的单色路径。虽然一般猜想仍然难以解决，但迄今为止的进展主要来自两个方面：有限情形和渐近松弛。最佳的有限结果归功于 Frankston 和 Scheinerman (2024)，他们使用 SAT 求解器验证了 $n \leq 7$ 的情形，而最佳的渐近结果归功于 Dvo\v{r}\'ak (2020)，他证明每个 $2$-色边着色的 $Q_n$ 都包含一条长度至少为 $n$ 且颜色变化至多 $0.375n + o(n)$ 的对偶路径。我们通过 SAT 方法在两个方面均取得改进：首先，通过引入更紧凑且更高效的 SAT 编码，结合对称破坏和 cube-and-conquer 并行技术，将验证范围扩展到 $n = 8$；其次，这种新编码的灵活性使我们能够将 Dvo\v{r}\'ak 的渐近方法的部分内容重构为 SAT 问题，从而将渐近上界提高到 $0.3125n + O(1)$ 颜色变化。我们的工作表明，SAT 方法不仅可以产生有限案例的确认，还能在组合猜想上取得渐近进展。