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

技術要約：充足可能性問題（Satisfiability）を用いた、$k$ 個の共線点を回避する北東格子経路の研究

問題の定義
本論文は、ジェルバー–ラムゼー（Gerver–Ramsey）の共線性問題を調査するものである。この問題は、北および東へのステップ（$\{(1,0), (0,1)\}$）からなる北東格子経路において、共線的な $k$ 個の点を含まない最大長を求めるものである。$a(k)$ を、長さ $a(k)$ のすべての北東格子経路が必ず $k$ 個の共線的な点を含むような最小の整数とする。したがって、$a(k)-1$ は、$k$ 個の共線的な点を回避する最長の経路の長さである。モンゴメリー（Montgomery, 1972）は、すべての $k$ に対してこのような境界が存在することを証明したが、ジェルバーとラムゼー（Gerver and Ramsey, 1979）は明示的ではあるものの極めて緩い上界を示したに過ぎない。そのため、$k$ が小さい場合の $a(k)$ の正確な値は、長らく不明であるか、あるいは計算による検証が困難であった。これに先立ち、J. Shallit（2013）は、計算によって $a(4)=9$、$a(5)=29$、$a(6)=97$ を決定し、$a(7) \ge 261$ という下限を、長さ 260 の経路を見つけることで確立していた。

手法
著者らは、これらの格子経路を列挙および検証するために、ブール充足可能性問題（SAT）ソルバを採用している。核心となるアプローチは、$k$ 個の共線的な点を回避する長さ $m$ の経路の存在を、論理積標準形（CNF）の公式としてエンコードすることである。

1. SAT エンコーディング:

   • 変数: ブール変数 $v_{x,y}$ は、点 $(x,y)$ が経路上の点であるかどうかを表す。
   • 経路制約: 経路が $(0,0)$ から始まり、北または東にのみ移動し、かつ分岐しない（すなわち、任意の点から、次に進むべき 2 つの候補のうち正確に 1 つの点へ進む）ことを保証する節（clause）を用いる。
   • 非共線性制約: いかなる直線も $k$ 個の点を含まないことを保証するために、カーディナリティ制約（at-most-$k$）を使用する。これらは、逐次カウンタ・エンコーディングを用いて CNF にエンコードされるか、あるいは「at-least-$k$ 結合標準形（KNF）」を用いて直接扱われる。
   • 最適化:
     • 対称性の破壊: 最初のステップを「北」に強制することで探索空間を縮小し、補元対称性を排除する。反転対称性については、エンコーディングのオーバーヘッドを避けるために探索中は主に無視されたが、列挙後の同型性チェックにおいて処理された。
     • 到達可能性の境界: 特定の方向へ $k-1$ 回連続して進む必要があるなど、到達不可能であることが証明された点は、単一節（unit clause）によってブロックされる。
     • 制約除去ヒューリスティック: ソルバの効率を高めるため、関連する領域内に非常に少ない点しか持たない直線に対応する非共線性制約を削除する。解が見つかった場合は、 $k$ 個の共線的な点が存在しないことを確認するために、明示的な検証が行われる。
     • 並列化: 大規模なインスタンスに対しては、「キューブ・アンド・コンカー（cube-and-conquer）」手法が使用される。先行ソルバ（march）が探索空間を互いに素な部分問題（キューブ）に分割し、それらを並列に解決する。

2. ソルバの選択:

   • 著者らは、標準的な CNF エンコーディング（CaDiCaL により解決）と KNF エンコーディング（Cardinality-CaDiCaL により解決）をベンチマークした。
   • 結果として、充足可能なインスタンス（長い経路を見つける場合）では KNF が大幅に優れた性能を示し、一方で充足不能なインスタンス（より長い経路が存在しないことを証明する場合）では CNF が優れていることが示された。手法としては、目的が経路の発見であるか、あるいはその非存在の証明であるかに基づいて、エンコーディングのタイプを適応させている。

主要な結果
本論文は、以下の計算結果を提示している。

• $k \le 6$ における列挙: 著者らは、$k \le 6$ について、同型を除いたすべての極大 GR($k$) ウォーク（長さ $a(k)-1$ の経路）を網羅的に列挙した。

  • 既知の結果を確認：$a(4)=9$、$a(5)=29$、$a(6)=97$。
  • 異なる極大 GR(4) ウォークが 2 つ、一意の極大 GR(5) ウォークが 1 つ、そして 2 つの異なる極大 GR(6) ウォークが存在することを発見した。
  • より長い経路の不在を証明するために DRAT 証明書を生成し、ソルバ自体を信頼することなく、結果を独立して検証可能にした。

• $k = 7$ に関する進展:

  • 下限の改善: 著者らは、長さ 327 ステップの GR(7) ウォークを発見し、Shallit によって見出された従来の最善の長さ 260 ステップを大幅に更新した。
  • 到達可能性解析: GR(7) ウォークについて 267 ステップまでの上界および下界の到達可能性を決定し、直線 $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. $a(7)$ の正確な値は依然として不明であるものの、SAT ソルバが以前の発見よりも有意に長い経路を見つけるために効果的に探索空間をナビゲートできること、および非存在の主張に対して証明書を生成できることの実証的な研究。

著者らは $a(7)$ の決定については謙虚な姿勢を保っており、その正確な値は依然として未知であるとしつつも、この問題への SAT ソルバの導入がさらなる進展を促進することを期待している。