💻 computer science

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

本論文は、ウィットネス分割、ウィンドウ基数による枝刈り、およびハイブリッドSAT/MIPソルバーを組み合わせた再現可能な計算フレームワークを提示し、 $r_3(212)$ の上界を厳密に調査することで、ほとんどの候補となる44集合を排除することに成功し、広範な検証作業にもかかわらず未証明のまま残された2つの耐性のある構造的ケースを特定したものである。

原著者： 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までの数字）に、できるだけ多くのアイテムを詰め込もうとしていると想像してください。ただし、一つ厳格なルールがあります：3つのアイテムが完璧な等差数列のパターンを作ってはならないというルールです。

例えば、もしあなたが「2」を選んだなら、「4」と「6」も選ぶことはできません。なぜなら、$2, 4, 6$ はそれぞれが前の数より2大きいというパターン（これは「3項等差数列」と呼ばれます）を形成しているからです。

数学者たちは、このルールを破らずに、どれだけ多くのアイテムをスーツケースに入れられるか、その絶対的な最大数を突き止めようとしてきました。スーツケースのサイズが211の場合、答えは43であることが知られています。今回の論文における大きな疑問は、**「サイズ212のスーツケースに44個のアイテムを入れることはできるのか？」**という点です。

著者であるメフメット・エルゲゼル（Mehmet Ergezer）は、単に推測したわけではありません。彼は、44個は不可能であることを証明するために、巨大なデジタル工場を構築しました。以下に、簡単な比喩を用いて、この論文の構成を解説します。

1. 戦略：「ウィットネス・スプリット（証人の分割）」工場

212個の中から44個の数字のあらゆる組み合わせをチェックしようとするのは、地球上のあらゆるビーチにある特定の砂粒を探すようなものです。一台のコンピュータで扱うにはあまりにも膨大すぎます。

そこで、著者は巧妙なトリックを用いました：

ウィットネス（証人）： 彼は、すでに成立していることが分かっている「安全な」43個のリストからスタートしました。
スプリット（分割）： その安全なリストから最も「重要な」24個の数字を取り出し、それらについてのあらゆる「Yes/No」のシナリオをコンピュータにチェックさせました。
結果： これにより、不可能なほど巨大なデータの山を、**1,250万個の管理可能な小さな塊（チャンク）**へと分解することができました。そして、コンピュータはこれらの塊を一つずつ解こうと試みました。

2. ツール：「ウィンドウ」と「リファインメント（洗練）」

コンピュータを高速化するために、著者は2つの特別なツールを追加しました。

ウィンドウ・カード（枝刈り）： スーツケースの小さなセクションを窓越しに覗き込む様子を想像してください。数学の既知のルールから、サイズ50の小さな窓には、例えば10個のアイテムしか入れられないことが分かっています。コンピュータはこのルールを利用して、その窓の中に11個のアイテムを入れようとする「塊」を即座に切り捨てます。これが最も強力なツールであり、困難な塊の数を30%近く削減しました。
リファインメント（深掘り）： もしある塊の解決に60秒以上かかった場合、コンピュータは諦めるのではなく、その特定の難しい塊に対してさらに多くのルールを適用し、より長い制限時間を与えて再挑戦しました。これは、鍵のかかった箱に対し、特定の鍵穴を選び、より大きな鍵を使って再び試みるようなものです。

3. 結果：「ハード・ポケット（困難なポケット）」

スーパーコンピュータのクラスター上で数百万回のチェックを実行した結果、以下のことが判明しました。

成功ゼロ： コンピュータは、44個のアイテムを詰めるための有効な方法を一度も見つけることができませんでした。試みるたびに、コンピュータは壁にぶつかり、「不可能」と回答しました。
エビデンス（証拠）： これは、44個は不可能であるという強力な証拠ではありますが、まだ正式な証明ではありません。なぜなら、制限時間内に解けなかった、いくらかの頑固な塊がまだ残っているからです。

「ハード・ポケット（抵抗するチャンク）」:
数百万の塊の中で、著者は非常に執拗な45個の塊のグループを見つけました。これらは、追加の時間を与えられても、異なるツールを使っても解決を拒みました。

LPアタック： 問題を滑らかな曲線として捉える別のタイプの数学ソルバー（HiGHSと呼ばれます）を試しましたが、これら45個の塊を一つも解くことはできませんでした。
CDCLアタック： 失敗から学ぶ探偵のように機能する、第三のソルバー（CDCLと呼ばれます）を試しました。これが成功し、45個のうち18個を解くことができました。
最後の2つ： しかし、2つの塊（T1cとラベル付けされたもの）は、依然として完全に未解決のまま残りました。これらは最初のソルバーにも、二番目のソルバーにも、三番目のソルバーにも抵抗しました。これらがこの問題の「ラスボス」です。

4. 結論：「ユニット・ギャップ（単位の隙間）」

論文は次のように結論付けています：

私たちは、成立することが確認されている43個の数字のリストを持っています。
コンピュータは何百万回も試みて失敗したため、44は不可能であるという強力な証拠があります。
しかし、これら2つの最後の頑固な塊があるため、まだ100%の数学的証明は得られていません。答えはほぼ間違いなく43ですが、43と44の間の「ギャップ」は、技術的にはまだ開いたままなのです。

5. コミュニティへの贈り物

著者は単に「諦める」のではなく、すべてのデータを公開しています。彼は、この2つの頑固な塊を、課題として世界に投げ出しています。

彼は、他の数学者がこれら2つの塊だけを解けるように、正確なコードとデータを提供しています。
さらに、問題を形式証明システム（Lean）用の言語に翻訳し、コンピュータ科学者が論理エンジンを用いて証明に挑戦できるよう招待しています。

要約すると： 著者は、パターンを持たない数字の詰め込み記録を破ろうとする、巨大なデジタルマシンを構築しました。そのマシンは記録を破る方法を見つけることはできませんでしたが、2つの小さく、信じられないほど困難なパズルで立ち往生してしまいました。論文はこう言っています。「私たちは、答えが43であると99.9%確信していますが、それを証明するために解くべき、これら2つの最後のパズルをここに置いておきます」

技術要約： $r_3(212)$ に対する Witness-Split + Window-Cardinality 精緻化

問題設定
本論文は、 $[1, N]$ 内の、非自明な3項等差数列（3-AP）を含まない部分集合の最大サイズとして定義される $r_3(N)$ の厳密な計算を取り扱う。漸近的挙動（Rothの定理やKelley–Mekaなど）は十分に研究されているが、ここでは $N=212$ という有限の境界に焦点を当てる。OEIS A003002に基づき、 $r_3(211) = 43$ である。著者らは、決定問題である「 $[1, 212]$ 内に要素数44の3-APフリーな部分集合は存在するか？」を調査している。
著者らは、43要素のウィットネス（証拠）を独立して検証しており、これにより $r_3(212) \ge 43$ を確立している。上界に関する問いは、 $r_3(212) \le 43$ かどうかである。仮定される44要素の集合が満たすべき必要条件は、両端の要素である1と212を含むことである。そうでなければ、それは $[1, 211]$ 内の44要素の集合へと変換され、既知の値と矛盾するためである。したがって、問題は $\{1, 212\}$ を含む44要素の集合の実行不可能性を証明することに帰着する。

手法およびアーキテクチャ
著者らは、実行可能な44要素の集合を探索するために、5つのコンポーネントを組み合わせた再現可能な計算フレームワークを提案している。

決定形式の CP-SAT モデル: 問題は $i \in [1, 212]$ に対するブール変数 $x_i$ を用いてエンコードされる。制約には以下が含まれる：
- 3-AP不等式：すべての3項等差数列を形成するトリプル $(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}$ を使用する。 $A_{43}$ の要素をそのAP出現次数によってランク付けし、上位24個を選択する。探索空間は、これら24個の変数の値を固定することで $2^{24}$ 個の「チャンク」に分割される。固定された接頭辞が3-APを強制する場合、多くのチャンクは即座に枝刈りされる。
Window-Cardinality Pruning（ウィンドウ・カーディナリティによる枝刈り）: 有効な不等式を導入することが重要な介入となる。任意のウィンドウ $[a, a+L-1]$ について、変数の和は $r_3(L)$ によって制限される。 $N=212$ の場合、これは22,154個の不等式を追加することになり、生の3-AP制約を超えてモデルを大幅に強化する。
再帰的精緻化: 広域レイヤー（深さ24）で UNKNOWN を返したチャンクは、次に次数が高いウィットネス変数を用いて固定接頭辞を拡張し（深さ40, 48, 56, 64）、より長いタイムキャップを設定して再解決することで精緻化される。
ソルバーの多様性とエンジニアリング: このキャンペーンは、UMass Unityクラスター上で動作するSLURMベースのパイプラインを利用している。以下のものを使用する：
- CP-SAT (OR-Tools): 広域パスおよび再帰的精緻化用。
- HiGHS (MIP): 最も困難な "UNKNOWN" チャンクを攻撃するために使用される、LP緩和に基づくMIPソルバー。
- CDCL/SAT (CaDiCaL): LP手法に対して抵抗力のあるチャンクを再攻撃するために使用され、不満足性のためのDRAT証明を生成する。

実証結果
キャンペーンは、深さ24のスウィープおよび様々な精緻化レベルにわたって、数百万のサブ問題を処理した。

実行可能な解の不在: テストされたすべてのサブ問題（広域パス、精緻化、HiGHS、およびCDCL）において、実行可能な44要素の集合はゼロであった。これは $r_3(212) = 43$ という予想を強力に支持するものであるが、形式的な証明ではない。
Window-Cardinality の影響: ウィンドウ・カーディナリティ不等式を有効にすることで、広域パスにおける UNKNOWN 率が約28パーセントポイント減少した（例：制御されたバッチにおいて約30%から1.65%へ）。これは最も効果的な枝刈りレイヤーであることを示している。
構造的な「ハード・ポケット」:
- 100,000チャンクの拡張バッチから、6,071個のチャンクが UNKNOWN を返した。
- これらのランダムサンプルに対する300秒のリカップにより、45個の抵抗力のあるチャンク（ティア T1）が残った。
- HiGHS による攻撃: 1時間のHiGHS実行では0/45を解決。8時間の監査により25/45を解決し、20個のチャンク（ティア T1b）が残った。これらは双対境界が0.0に固定されており、LP緩和が実行不能の証明を提供できないことを示している。
- CDCL による攻撃: 20個の T1b チャンクに対する純粋な CDCL/SAT 攻撃により、18/20を解決し、独立して検証可能なDRAT証明を生成した。
- 残留物 (T1c): 2つのチャンク（ID 40959 および 48895）は、12時間の純粋なCDCL実行および4時間のウィンドウ付きCDCL診断の後でも UNKNOWN のまま残った。これら2つのチャンクは、CP-SAT、HiGHS (LP-MIP)、およびCDCLのパラダイムすべてに対して抵抗を示している。

主な貢献
本論文は、その貢献を $r_3(212)$ の新しい厳密な値ではなく、方法論的なものであると明示的に位置づけている。具体的な貢献は以下の通りである：

アーキテクチャ: ウィットネス分割、ウィンドウ・カーディナリティによる枝刈り、および再帰的精緻化を組み合わせた、厳密な上界探索のための再現可能なフレームワーク。
実証的記述: $N=212, K=44$ キャンペーンの詳細な分析（ソルバーのトレードオフや、特定のピン割り当てを持つ「ミドルアウト」チャンクの非一様性などを含む）。
ハード・ポケットの特性把握: 一般的なソルバーのパラダイム（CP-SAT, HiGHS, CDCL）の下で、寛大な時間制限を用いても不変である構造的な障害（T1c）の特定。
ベンチマークのリリース: 階層化されたインスタンスのリリース：
- T1a: HiGHS によって解決された25個のチャンク。
- T1b \ T1c: DRAT証明を伴うCDCLによって解決された18個のチャンク。
- T1c: 最終的な抵抗力を持つ2つのチャンク。これらは最も鋭い未解決問題として提示される。
- T2/T3: 6,071個の広域 UNKNOWN および将来の試みのための全12.5Mチャンクジェネレータ。
形式化: 形式的証明探索システムのための、T1c ターゲットの Lean 4 エンコーディング。

意義および主張
著者らは、このキャンペーンは $r_3(212) = 43$ という予想を強く支持するものの、解決されていない T1c の残留物があるため、形式的な証明にはならないと控えめに主張している。その意義は、具体的な計算上の障壁を孤立させたことにある：

証明された境界のギャップは正確に1である（ $43 \le r_3(212) \le 44$ ）。
LPベースの手法（HiGHS）の失敗とCDCLの部分的な成功は、この困難さが単なる伝播のアーティファクトではなく、LP緩和のギャップがタイトであり、整数実行不能性の証明が組合せ論的に拡散しているという構造的特性であることを示唆している。
論文は、このギャップを埋めるには、より強力な加法的組合せ論的境界（例：フーリエ解析的またはマルチウィンドウ分割境界）か、一般的なソルバーでは捉えきれない問題固有の対称性を利用するカスタムの分岐限定法システムが必要であると断じている。

本研究は、汎用的な組合最適化ソルバーの限界を示すベンチマークとして、特定の検証済みインスタンス（T1c）を提供しており、このクラスの問題における現在の限界を象徴している。