North-East Lattice Paths Avoiding $k$ Collinear Points via Satisfiability

技术摘要：通过可满足性问题研究避免 $k$ 个共线点的北–东格点路径

问题定义
本文研究了 Gerver–Ramsey 共线性问题，该问题旨在确定不包含 $k$ 个共线点的北–东格点路径（步进集合为 $\{(1,0), (0,1)\}$）的最大长度。令 $a(k)$ 表示最小整数，使得每一条长度为 $a(k)$ 的北–东格点路径都包含 $k$ 个共线点；因此，$a(k)-1$ 是避免 $k$ 个共线点的最长路径长度。虽然 Montgomery (1972) 证明了对于所有 $k$ 这样的界限都存在，且 Gerver 和 Ramsey (1979) 提供了一个显式但极其宽松的上界，但对于较小的 $k$，精确的 $a(k)$ 值在很大程度上仍是未知的，或在计算上难以验证。在此项工作之前，J. Shallit (2013) 通过计算确定了 $a(4)=9$、$a(5)=29$ 和 $a(6)=97$，并利用找到一条长度为 260 的路径建立了 $a(7) \ge 261$ 的下界。

方法论
作者采用布尔可满足性 (SAT) 求解器来枚举并验证这些格点路径。核心方法是将存在一条避免 $k$ 个共线点的长度为 $m$ 的路径这一问题，编码为一个合取范式 (CNF) 公式。

1. SAT 编码：

   • 变量： 布尔变量 $v_{x,y}$ 表示点 $(x,y)$ 是否在路径上。
   • 路径约束： 子句确保路径从 $(0,0)$ 开始，仅向北或向东移动，且不会发生分裂（即从任何一点出发，路径恰好走向两个可能下一个点中的一个）。
   • 非共线性约束： 作者使用基数约束（最多-$k$）来确保没有任何直线包含 $k$ 个点。这些约束通过顺序计数编码被编码进 CNF，或者通过使用 klauses 的“至少-$k$ 合取范式 (KNF)”进行原生处理。
   • 优化措施：
     • 对称性破缺： 通过强制第一步向北来减少搜索空间，从而消除了补集对称性。在搜索过程中，反转对称性在很大程度上被忽略，以避免编码开销，同构检查是在枚举后进行的。
     • 可达性界限： 被证明不可达的点（例如，那些需要连续 $k-1$ 步沿同一方向移动的点）通过单位子句被阻断。
     • 约束移除启发式算法： 为了提高求解器效率，移除了对应于在相关区域内点数极少的直线的非共线性约束。如果找到了解，会进行显式验证以确保不存在 $k$ 个共线点。
     • 并行化： 对于大型实例，使用“分而治之”（cube-and-conquer）技术。一个前瞻求解器 (march) 将搜索空间划分为不相交的子问题（cubes），然后并行求解这些子问题。

2. 求解器选择：

   • 作者将标准的 CNF 编码（由 CaDiCaL 求解）与 KNF 编码（由 Cardinality-CaDiCaL 求解）进行了基准测试。
   • 结果表明，KNF 在可满足实例（寻找长路径）上表现显著更好，而 CNF 在不可满足实例（证明不存在更长的路径）上表现更优。该方法根据目标是寻找路径还是证明其不存在来调整编码类型。

关键结果
本文展示了以下计算结果：

• $k \le 6$ 的枚举： 作者穷举了所有直到同构意义下的极大 GR($k$) 走法（长度为 $a(k)-1$ 的路径），针对 $k \le 6$ 的情况。

  • 确认了之前的研究结果：$a(4)=9$、$a(5)=29$ 以及 $a(6)=97$。
  • 发现存在两个不同的极大 GR(4) 走法，一个唯一的极大 GR(5) 走法，以及两个不同的极大 GR(6) 走法。
  • 生成了 DRAT 证明证书，用于验证不存在更长路径的结果，从而实现无需信任 SAT 求解器本身的独立验证。

• $k = 7$ 的进展：

  • 下界改进： 作者发现了一条长度为 327 步的 GR(7) 走法，显著提升了此前 Shallit 发现的 260 步的最长已知长度。
  • 可达性分析： 他们确定了高达 267 步的 GR(7) 走法的上界和下界可达性，并确定了直线 $y=x+1$ 上的第一个不可达点为 $(146, 147)$。
  • 搜索策略： 最长的走法是通过涉及随机种子并行化和“分而治之”的混合方法找到的。值得注意的是，发现的最长走法集中在 $y=x+1$ 线附近。

意义与主张
本文声称，SAT 求解器不仅能有效解决具有巨大搜索空间的离散几何问题，而且由于能够生成并验证证明证书（DRAT 格式），其提供的可信度比自定义编写的搜索代码更高。

主要贡献包括：

1. 一种用于寻找长 GR($k$) 走法并证明其极大性的基于 SAT 的方法。
2. 对 $k \le 6$ 的所有极大 GR($k$) 走法进行了完整枚举，确认并扩展了之前的计算结果。
3. 一个新的 $a(7)$ 下界，将已知最长路径从 260 步扩展到了 327 步。
4. 一项实验研究，证明了尽管通过 SAT 求解可以有效地导航搜索空间以找到比以往发现的更长的路径，但对于非存在性声明，也可以生成证明证书。

作者对确定 $a(7)$ 的做法保持谦逊，指出其精确值仍然未知，但希望他们将 SAT 求解引入该问题能促进进一步的进展。