An Efficient MaxSAT-DDD Approach for Train Rescheduling via Precedence Propagation and Hybrid AMO Encodings

技術要約：列車再スケジューリングのための効率的なMaxSAT-DDDアプローチ

問題定式化
本論文は、乱れた時刻表を修正することを目的とした、固定ルート列車再スケジューリング問題（TRP）を扱っている。この問題では、列車の経路の優先順位、リソース容量制約を遵守しつつ、遅延目的関数を最小化する。本モデルは列車のルートを固定していることを前提としており、これにより探索空間は簡素化されるが、ルート変更を必要とする大規模な混乱への適用性は制限される。モデルには以下が含まれる：

• 優先順位制約： 列車の経路に沿った操作の順序を保証する。
• リソース安全性： 列車の同一リソース（ブロック区間、線路、または駅）への同時占有を防ぐための非分離制約。
• 遅延目的関数： 3つのコスト関数（ステップ関数型：特定の閾値超過に対するペナルティ、丸め型：180分単位の粒度に基づくペナルティ、連続型：線形遅延コスト）を評価する。

著者らは、完全な時間離散化に伴う計算の困難さを回避するために、**動的離散化発見（Dynamic Discretization Discovery: DDD）**を利用している。代わりに、DDDは制限された時間インデックス・モデルを解き、実現可能性と最適性を証明するために必要なタイムポイントのみを反復的に精緻化する。

手法
コアとなる貢献は、精緻化ループの中に2つの特定の改善策を統合した、強化されたMaxSAT-DDDエンコーディングである。

1. リソース競合のためのハイブリッドAMO（At-Most-One）エンコーディング：

   • リソース競合は、時間依存の占有クリーク（clique）としてモデル化される。
   • 著者らは、標準的なペアワイズ（対）排除（$\Theta(n^2)$ 個の節を生成する）を、ハイブリッドなアプローチに置き換えた。小規模なクリーク（$n < 6$）についてはペアワイズの節を維持し、大規模なクリークについては、節の数を線形複雑度（$O(n)$）に削減するSinzの逐次カウンタ（sequential-counter）エンコーディングを採用している。
   • このエンコーディングは、特定の時刻に列車がリソースを占有しているかどうかを定義する「ラダーリテラル（ladder literals）」に指示変数（indicator variables）をリンクさせる。

2. 列車経路の優先順位伝播：

   • 最初のDDDイテレーションの前に、ソルバーはフォワードパスを実行し、各列車のルートにおける有効な開始時刻（$t^{eff}$）を計算する。
   • この伝播により、ある操作の開始時刻は、先行する操作の終了時刻に走行時間を加えたもの以上でなければならないという制約を課すことで、初期の下限ラダーをタイトにする。
   • この前処理ステップは、全ルート長に対して線形であり、実行可能なスケジュールをすべて保持しながら、探索空間を早期に削減する。

ソルバーアーキテクチャ
提案されたソルバーであるMaxSAT-Defaultは、これら2つの改善策を組み合わせている。これは、以下のプロセスを交互に行うDDDループ内で動作する：

1. 制限された重み付き部分MaxSATインスタンス（実現可能性のためのハード節、遅延コストのためのソフト節）を解く。
2. 解をデコードして違反を確認する。
3. 違反または目的関数の不一致が見つかった場合、時間間隔を精緻化し、新しいパス/リソース/コストの節を追加する。
   本研究では、これをベースラインとなるMaxSATエンコーディング、増分および非増分SATバックエンド（RC2、Glucose 4.2）、およびBig-M MILP、時間インデックス（TI）MILP、制約プログラミング（CP）定式化を用いた商用ソルバー（Gurobi、CPLEX）と比較している。

主な貢献

• エンコーディングの効率性： 大規模なリソースクリークに対する逐次カウンタAMOエンコーディングの統合により、CNFのサイズが大幅に削減され、ペアワイズエンコーディングと比較して単一伝播（unit propagation）の速度が向上した。
• 探索空間の削減： 優先順位伝播によって初期境界がタイトになり、特に連続遅延目的関数において、DDDのイテレーション数とソルバーのバックトラッキングが減少した。
• 実証的評価： 3つの遅延目的関数にわたる72のインスタンスを用い、4つのMaxSATバリアントを最先端のMILPおよびCPベースラインと比較した包括的な評価を行った。

実験結果
実験は、ノルウェーのベルゲン線から派生したベンチマークを用いて行われ、25〜30本の列車と、変動するレベルのリソース集約（オリジナル、線路、駅）を特徴としている。

• ステップ関数型目的関数： MaxSAT-Defaultは72インスタンスすべてを解決し、平均実行時間は23 msであった。これはGurobiのBig-M MILPの解決数と一致したが、平均して約16倍高速であった。
• 丸め型目的関数： MaxSAT-Defaultは、解決したインスタンス数を変えることなく、平均実行時間を794 ms（ベースライン）から479 msに短縮した。困難な連続トラックインスタンスにおいて、アブレーション研究では、共通解決サブセットにおいて最大79.6%の実行時間削減を示した。
• 連続型目的関数： 連続遅延についてはBig-M MILP（Gurobi）が依然として最強のベースラインであったが、MaxSAT-DefaultはベースラインのMaxSATエンコーディングを上回り、解決数は59件に対し60件となり、実行時間も短縮された。
• 困難なインスタンス： 密な集約インスタンス（例：trackA8, stationA8）において、MaxSAT-Defaultは一貫してベースラインを上回り、タイムアウトやメモリ枯渇が発生したTI-MILPやCPのアプローチをしばしば凌駕した。

意義と主張
本論文は、提案されたMaxSAT-DDDアプローチが離散的な遅延目的関数（ステップ関数型および丸め型）に対して非常に効果的であり、ベースラインのMaxSATと比較して大幅な高速化を実現し、商用MILPソルバーに対しても競争力のある性能を提供すると主張している。著者らは、固定ルートの仮定が軽微な遅延回復への適用範囲を限定する一方で、本研究は、この領域における厳密解法のための必要な基礎を提供するものであると述べている。

研究の控えめな結論として、連続的な遅延目的関数についてはBig-M MILPが依然として優位であり、MaxSATアプローチは下限を強化することよりも、困難なサブセットにおける探索を加速することに価値があるとしている。提案されたエンコーディングの主な価値は、リソース集約を効率的に処理し、DDD精緻化ループの計算オーバーヘッドを削減できる能力にある。今後の課題として、ルート変更を扱うためのモデルのスケーリング、および連続コストに対する下限の強化が挙げられている。