Constant time testability of first-order logic with modulo counting on finitary graphs

技術的サマリー：有限グラフにおけるモジュロ計数付き第一階述語論理の定数時間テスト可能性

問題提起
本論文は、有界次数グラフモデルにおける性質テストの課題、特に入力サイズ $n$ に依存しない定数実行時間を保証するアルゴリズム的メタ定理の追求に焦点を当てている。Adler と Harwath（2018）による先行研究は、有界次数かつ有界木幅（$C^w_d$）を持つグラフクラスにおいて、計数付き単項第二階述語論理（CMSO）が多対数実行時間でテスト可能であることを確立したが、これを定数時間に改善できるかどうかは未解決の問題であった。

本論文は、最大次数が $d$ で、すべての連結成分のサイズが定数 $c$ で有界であるグラフのクラスとして定義される有限グラフクラス（$C^c_d$）において、この問いを検証する。著者らは、モジュロ計数付き第一階述語論理（FOMOD）で表現可能な性質、およびそれに続く CMSO が、これらのクラス上で定数実行時間でテスト可能かどうかを決定することを目指す。

手法
著者らは、定数時間テスターを構築するために、論理的正規形、確率的サンプリング、および数論的技法の組み合わせを採用する。

1. 特化された Hanf 正規形:
   証明は、FOMOD 式に対する特定のバージョンの Hanf 正規形に依存する。著者らは、Hanf の局所性定理を有限グラフの設定に適応させる。彼らは、$C^c_d$ 上の任意の FOMOD 文 $\phi$ を、原子式が特定の連結成分タイプ（サイズ $\le c$ の同型タイプ）の存在と特定の個数を記述する論理和標準形（DNF）に変換できることを示す。

   • 決定的な点として、量化子は単一の半径（$c-1$）と一様な「上限」$k$ に統一される。
   • 式の充足性は、グラフの成分ヒストグラムベクトルが特定の制約を満たすかどうかの検査に帰着される。

2. 上限付き成分ヒストグラムベクトル（k-CCHV）:
   著者らは、連結成分の同型タイプでインデックス付けされた $k$-上限付き成分ヒストグラムベクトル $a$ を定義する。各タイプ $t$ に対して、エントリ $a[t]$ はグラフ内での $t$ の出現数に関する制約を指定する。

   • 希少なタイプ: 個数は $0$から$k-1$ までの整数と等しい。
   • 頻出タイプ: 個数は $k$ 以上であり、特定の合同条件（$\equiv j \pmod m$）を満たす。
     主要な論理的結果（補題 14）は、$C^c_d$ 内のグラフが FOMOD 文を充足するならば、かつそのグラフの成分ヒストグラムベクトルがその文から導出された有限集合 $X$ の少なくとも一つのベクトルを充足するならば、そのグラフがその文を充足するということである。

3. アルゴリズム的戦略:
   提案されたテスターは 2 つのフェーズで動作する。

   • サンプリング: アルゴリズムは定数個の頂点をサンプリングし（$\epsilon, c, d$ によって決定される）、それらの連結成分を探索して成分タイプの頻度を推定する。
   • 検証:
     • サンプル内で「希少な」成分タイプ（存在しないか、少量で存在することが要求される）が検出された場合、アルゴリズムは棄却する。
     • 希少なタイプが検出されない場合、アルゴリズムは算術的検査を行う。これは、頂点の総数 $n$ がヒストグラム制約を満たすグラフの構築を可能にするかどうかを検証する。これには、フロベニウスの硬貨定理から導出された整除性の条件が含まれる。具体的には、必要な希少な成分と最小限の頻出成分を考慮した後の残りの頂点が、頻出成分タイプのサイズの錐的結合（conical combination）で埋め尽くせるかどうかを検査する。

4. 数論的「パッチ可能性」:
   重要な技術的貢献は、フロベニウスの硬貨定理の使用である。正しさを証明するために、著者らは、グラフが性質から「遠い」場合、その性質を充足し入力から $\epsilon$-近い「パッチ済み」グラフ $G'$ を構築できることを示す。この構築には、必要な希少な成分を「植える」ことと、グラフの残りを頻出成分のコピーで埋めることが含まれる。フロベニウス数は、必要な数論的条件が満たされれば、十分に大きな $n$ に対して、残りの頂点数が常に頻出成分のサイズの和として表現できることを保証する。

主要な貢献と結果

• 主要定理（定理 16）: FOMOD で定義可能なすべての性質は、次数 $\le d$ かつ成分サイズ $\le c$ のグラフのクラス $C^c_d$ 上で定数実行時間でテスト可能である。
• 系（系 17）: 有限グラフクラスにおいて FOMOD と CMSO は同じ表現力を持つため、CMSO で定義可能なすべての性質も $C^c_d$ 上で定数実行時間でテスト可能である。
• 関係構造への拡張（定理 18）: この結果は、有界次数かつ有界成分サイズを持つ関係構造に一般化される。

意義と主張
本論文は、有界次数かつ有界木幅を持つクラスにおける CMSO の定数時間テスト可能性という未解決問題の解決に向けた重要な一歩であると主張している。

• 自然なステップ: 著者らは、有限クラスがまさに有界次数と有界木深さ（木幅よりも強い条件）の交点であることを指摘する。したがって、この研究はより広範な未解決問題への「自然なステップ」を提供する。
• 超有限グラフの基盤: 有限グラフは、定数時間テスト可能な性質を持つことが知られている超有限グラフの定義の中心にあるため、この研究はより大きく複雑なグラフクラスにおける定数時間テスト可能性を探求するための「礎石」として機能する。
• 「パッチ可能性」の独立性: 著者らは、局所サンプリングからの算術的検査によるグローバルな推論を可能にする数論的「パッチ可能性」条件が、独立した関心対象となり得ることを強調する。
• 限界: 本論文は、成分サイズが一様に有界でない一般的な有界木幅クラスについては、依然として未解決であることを謙虚に認めている。困難は、標準的な有界次数モデルに内在する制約、すなわち性質を満たすために頂点数を変更できない場合に特に生じる。

本論文は一般的な有界木幅の場合を解決したとは主張していないが、成分サイズが一様に有界である場合、局所サンプリングとグローバルな算術的制約の相互作用を活用することで、多対数時間から定数時間への移行が達成可能であることを確立している。