A SAT-Based Exact Approach for Radio k-Labeling

技術要約：Radio $k$-LabelingのためのSATに基づく厳密なアプローチ

問題の定義
本論文は、チャネル割り当て問題から派生した組合せ最適化問題であるradio $k$-labeling問題（radio $k$-coloringとも呼ばれる）を扱う。連結グラフ $G=(V, E)$ とその直径 $k = \text{diam}(G)$ が与えられたとき、目的は、すべての異なる頂点ペア $u, v$ に対して、条件 $|f(u) - f(v)| \ge k + 1 - d(u, v)$ が成り立つように、非負整数ラベル $f(v)$ を各頂点に割り当てることである。ここで $d(u, v)$ は最短経路距離である。目標は、ラベル付けのスパン（span）、すなわち $\max_{v \in V} f(v)$ を最小化することである。最小のスパンはradio numberと呼ばれ、$rn(G)$ と表記される。

特定のグラフ族（パス、サイクル、木など）については理論的な構成が存在し、一般的なグラフに対しては実行可能な解を提供するヒューリスティックアルゴリズムも存在するが、広範なグラフクラスに対する厳密解は依然として乏しい。既存の整数線形計画法（ILP）定式化は、探索空間の急速な増大と、最適化の反復間における情報の再利用の欠如により、スケーラビリティの問題に直面している。

手法
著者らは、コンパクトな順序エンコーディング（order encoding）と反復的な最適化戦略を組み合わせた、厳密かつ増分的なSATベースのフレームワークを提案している。

1. SATエンコーディング:
   本論文では、事前計算された上限 $UB$に基づくラベル領域${1, \dots, UB}$ を用いた2種類のブール充足可能性（SAT）エンコーディングを開発している：

   • 直接エンコーディング (Direct Encoding): 割り当て変数 $x_{v,l}$（頂点 $v$ がラベル $l$ を持つ場合に真）を使用する。これは、ペアごとの競合節によって制約を強制する。論理的にはILPモデルと等価であるが、radio制約のために $O(n^2 UB k)$ 個の節を必要とし、ユニット分解（unit resolution）の下での伝播が弱くなる。
   • 順序エンコーディング (Order Encoding): 割り当て変数とともに、閾値変数 $g_{v,l}$（$f(v) \ge l$ である場合に真）を導入する。このエンコーディングは、radio制約 $|f(u) - f(v)| \ge \Delta_{uv}$ をよりコンパクトに表現できる。これにより、節の数を $O(n^2 UB k)$ から $O(n^2 UB)$ へと削減し、$k$ への依存性を排除している。また、順序エンコーディングは、不等式 $f(v) \ge c$ が単一のリテラルにマッピングされるため、より強力な伝播を可能にする。

2. 増分的解決戦略 (Incremental Solving Strategy):
   本フレームワークは、増分的SATソルビング・パラダイムを採用している。各反復ごとに数式を再構築するのではなく、単一のソルバーインスタンスを一度構築する。アルゴリズムは以下の手順で進行する：

   • フェーズ1: 全対最短経路距離を計算し、$k = \text{diam}(G)$ を設定する。
   • フェーズ2: 初期上限 $UB$ を用いてSATモデルを構築する。
   • フェーズ3: 数式を反復的に解く。もしスパン $\beta$ を持つ充足可能な割り当てが見つかった場合、ソルバーに対してスパン $\ge \beta$ を禁止（上限を絞り込み）し、再解法を行う。極めて重要な点として、**学習された節（learned clauses）**は前回の反復から保持され、冗長な探索作業を回避する。ループは、ソルバーがUNSATを返して（最適性を証明して）終了するか、時間制限に達したときに終了する。

3. 対称性の打破 (Symmetry Breaking):
   回転対称性を持つサイクルグラフ ($C_n$) に対して、著者らは最初の頂点のラベルを1に固定する（$f(0)=1$）対称性の打破制約を導入している。これにより、最適解を破棄することなく、探索空間を縮小し、最適性の証明を大幅に加速させている。

主な貢献

• 新しいフレームワーク: 順序エンコーディングと増分的解決を利用した、radio $k$-labeling問題のための初の一般的な厳密SATベースの最適化フレームワーク。
• 効率性の向上: 順序エンコーディングにより、直接エンコーディングと比較して節の複雑さが軽減され、伝播が改善された。増分的アプローチは学習された節を再利用するため、独立したSAT呼び出しや標準的なILPアプローチと比較して、計算オーバーヘッドを大幅に削減できる。
• 対称性の処理: サイクルグラフに対する特定の対称性の打破制約の導入により、解法時間の短縮と、証明された最適解の数の増加を実現した。

実験結果
本フレームワークは、9つのグラフファミリー（パス、サイクル、三角蛇、$kC_m$-snake、ラダー、ブック、友情グラフ、二項木）にわたる146個のベンチマークインスタンスを用いて、1,200秒の制限時間で評価された。

• ヒューリスティックとの比較: 提案手法である Order-SAT は、既知の閉形式の最適解がない98個のインスタンスにおいて、38個の新しい最良既知のradio numberを確立した。これは、既存のヒューリスティック（Ub1, Ub3）や直接エンコーディングSATよりも一貫してタイトな実行可能境界を生成した。
• ILPとの比較:
  • 直径が増大するグラフ: 直径がサイズとともに増大するグラフ（snake、ladder、binomial treeなど）において、Order-SATは解の質（よりタイトな境界）および証明された最適解の数の両面で、商用ILPソルバー（CPLEX, Gurobi）を上回った。ILPソルバーは、これらのインスタンスにおいてメモリを使い果たすか、緩いインカンベント（暫定解）を返した。
  • 直径が一定のグラフ: 直径が一定のグラフ（book、friendshipグラフなど）では、ILPソルバーの方が効果的であり、すべてのインスタンスに対して迅速に最適性を証明した。
• 複合的アプローチ: SATフレームワークとILPモデルを組み合わせることで、本研究は146個中109個のインスタンスに対して最適解を証明し、最適性が証明されたradio-labelingベンチマークを大幅に拡大した。
• 統計的有意性: フリードマン検定により、Order-SATが商用ソルバーやヒューリスティックを含む比較対象の手法の中で、最高の総合ランキング（平均ランク 2.58）を達成したことが確認された。

意義
本論文は、増分的SATソルビングが、伝統的に理論的構成とヒューリスティックアルゴリズムに支配されてきたグラフラベル問題に対する、実用的な厳密最適化パラダイムを構成していると主張している。本研究は以下を実証している：

1. 現代的なSATソルバーは、コンパクトなエンコーディングと増分的戦略を組み合わせることで、従来のILP定式化がスケーラビリティに苦しむ困難な組合せ最適化問題を解決できる。
2. 提案されたアプローチはILPを補完するものである。直径が増大するグラフには優れており、一方で直径が限定的なグラフにはILPが適している。
3. 本フレームワークは、理論的な境界と厳密な解の証明との間の溝を埋めることに成功しており、複雑なグラフ構造におけるradio numberを決定するための堅牢なツールを提供している。

著者らは、このアプローチが特定のグラフクラスにおいて商用ソルバーに対して非常に競争力のある代替手段を提供することを結論付けており、他のグラフラベル問題や組合せ最適化問題に対する増分的SATソルビングの可能性を強調している。