本研究は、一部のエージェントに目的地が与えられない「Unassigned Agents in Multi-agent Path Finding (UA-MAPF)」という新しい問題設定を扱う。標準的なMAPFでは全エージェントが始点から終点への経路を必要とするが、UA-MAPFでは未割り当てエージェント $\mathcal{U}$ は目的地に到達する必要がなく、衝突回避のために必要に応じて移動するのみである。目的関数には、サービス完了時間の総和であるSST、全エージェントの移動回数の総和であるFUEL、移動する未割り当てエージェントの数であるNUA、および待機コストを考慮したFUEL+が定義される。本研究の焦点は、この問題をSATやSMTといった充足可能性問題に変換して解く「コンパイルベース」の手法への適応にある。
既存のコンパイルベースのMAPF手法に対し、UA-MAPFを扱うための定式化と適応方法を提案した。具体的には、反例誘導型抽象化洗練（CEGAR）に基づくSMT-CBSおよび、非洗練抽象化（non-refined abstractions）を用いるNRF-SATをUA-MAPFへ適合させた。適応にあたっては、MDDの構築プロセスにおいて、未割り当てエージェントに対してゴールからの距離制約を適用しない「UA-MDD」を導入するだけで済むことを示した。これにより、コンパイルベース手法のモジュール性と適応性の高さ、および未割り当てエージェントの存在が制約の緩和に与える影響についての知見を提供した。
MAPFをSATへ帰着させるため、Time Expanded Graph (TEG) を拡張したMDDを利用する。通常のMDDでは、頂点 $v$ が時刻 $t$ においてエージェント $i$ にとって到達可能である条件として $dist(s_i, v) \le t$ かつ $dist(v, g_i) \le T - t$ を用いて変数を制限する。しかし、目的地 $g_i$ を持たない未割り当てエージェントには後者の制約が適用できないため、開始地点からの距離 $dist(s_i, v) \le t$ のみに基づく「UA-MDD」を定義して使用する。ソルバーとしては、Glucose SATソルバーを基盤としたC++実装のSMT-CBSおよびNRF-SATを用い、NRF-SATではパス一貫性制約を省略してDAGを抽出する手法をとる。
AMD Ryzen 7 2700 (3.2GHz), 32GB RAMの環境下で、movingai.comの4つのマップ（empty-16-16, random-32-32-20, room-64-64-16, ost003d）を用いて実験を行った。各設定につき25回のランダム測定の平均値を評価指標としている。実験の結果、未割り当てエージェントの増加は、問題の緩和（制約の減少）とUA-MDDの巨大化という相反する影響を与えることが判明した。多くのマップでは、初期段階ではUA-MDDの増大による計算コストの増加が顕著だが、未割り当てエージェントの数が十分に大きくなると緩和効果が上回り、計算時間が減少する傾向が確認された。特にNRF-SATは、非精緻化抽象化により数式の巨大化を抑えられるため、SMT-CBSよりもUAの影響を受けにくい高い効率性を示した。
未割り当てエージェントの存在は、直感に反して計算量に複雑な影響を与える。エージェントの過半数が未割り当てになると緩和効果が上回り計算時間が減少するが、それまではUA-MDDのサイズ増大が支配的となる。例えば、小さなマップであるempty-16-16では、UA-MDDのサイズによる負の影響が軽微であるため、緩和効果が初期から現れるという特異な挙動が見られた。本研究により、コンパイルベースのMAPFソルバーは、MDDの生成ロジックをわずかに変更するだけでUA-MAPFへ容易に適応できることが実証された。今後の課題として、連続的な空間におけるMAPF問題へのUA-MAPFの導入が挙げられている。
本研究では、一部のエージェントには目的地が与えられ、残りのエージェントには目的地が与えられない「未割当エージェントが存在するMAPF（UA-MAPF）」という問題設定を扱う。UA-MAPFにおける未割当エージェントは、目的地に到達する必要はないものの、標準的なエージェントの経路を妨げないよう、必要に応じて移動させなければならないという特有の課題を持つ。著者らは、このUA-MAPFが、近年のコンパイルベースのMAPF手法を用いて定式化可能であることを示す。具体的には、反例誘導型抽象化洗練（CEGAR）に基づく SMT-CBS や、非洗練抽象化に基づく NRF-SAT といった、問題を充足可能性問題（SAT）として定式化する最新のソルバーを適応させる手法を提案している。
Multi-agent Path Finding (MAPF) は、無向グラフ上でエージェントが衝突を避けながら各々の始点から終点へ到達する経路を求める問題であるが、本論文では割り当てられたエージェントの集合 $\mathcal{A}$ に加え、目標を持たない未割り当てエージェントの集合 $\mathcal{U}$ を導入した Unassigned Agents MAPF (UA-MAPF) を扱う。UA-MAPF の目的関数には、割り当てられたエージェントのサービス完了時間の総和である Sum of Service Time (SST)、全エージェントの移動回数の総和である FUEL、移動する未割り当てエージェントの数である NUA、および待機コストを考慮した FUEL+ が定義される。本研究では、MAPF を SAT や MILP などの既存の形式に変換して解くコンパイルベースの手法に着目し、特に制約を意図的に省略する Lazy Compilation や、パス一貫性制約を省略して DAG を抽出する NRF-SAT のような非洗練抽象化（non-refined abstractions）の概念を UA-MAPF へ適応させる。具体的には、SMT-CBS および NRF-SAT ソルバーを UA-MAPF に適合させることで、コンパイルベース手法のモジュール性と適応性を実証する。実験評価を通じて、未割り当てエージェントの存在が制約の緩和に与える、直感に反する影響についての知見を提示している。
MAPFをSATへ帰着させる手法として、Time Expanded Graph (TEG) と Multi-Valued Decision Diagram (MDD) が用いられる。TEGはグラフ $G=(V, E)$ とmakespan $T$ に対し、各時刻 $t \in \{0, \dots, T\}$ ごとに頂点のコピーを導入した有向非巡回グラフであり、エージェント $i$ が時刻 $t$ に頂点 $v$ にいることを示すために、Boolean変数 $x_{i,v,t}$ を定義する。しかし、TEGは到達不能な頂点まで変数として保持するため非効率であり、実用的な手法では、頂点 $v$ が時刻 $t$ においてエージェント $i$ にとって到達可能である条件、すなわち $dist(s_i, v) \le t$ かつ $dist(v, g_i) \le T - t$ を用いて変数を制限したMDDが利用される。MDD-SATアルゴリズムは、下限値 $T_{min} = \max_i dist(s_i, g_i)$ から開始して $T$ をインクリメントすることでmakespan最適性を保証するが、FUEL+コストの最適化には $T$ に加えてコストの境界値も増分させる手法が取られる。本研究が扱う「割り当てられていないエージェント (Unassigned Agents)」は、特定のゴールを持たないため、MDDのサイズ削減においてゴールからの距離に基づく制約（式2の後半部分）を適用できず、開始地点からの距離に基づく制約のみを適用した「UA-MDD」として定義される。
本実験では、C++で実装された SMT-CBS および NRF-SAT ソルバーを用い、Glucose SAT ソルバーを基盤として未割り当てエージェント（UA）を含む UA-MAPF の性能を評価している。実験は AMD Ryzen 7 2700 (3.2GHz), 32GB RAM の環境下で、movingai.com ベンチマークの 4 つのマップ（empty-16-16, random-32-32-20, room-64-64-16, ost003d）を用いて行われ、各設定につき 25 回のランダム測定の平均値が算出されている。未割り当てエージェントの増加は、問題の緩和（relaxation）と、UA-MDD（Unassigned Agent Multi-valued Decision Diagrams）の巨大化という、相反する二つの影響をソルバーに与える。実験結果によれば、多くのマップにおいて、初期段階では UA-MDD の増大による計算コストの増加が顕著であるが、未割り当てエージェントの数が十分に大きくなると緩和効果が上回り、計算時間が減少する傾向が確認された。特に、小さなマップである empty-16-16 では UA-MDD のサイズによる負の影響が軽微であるため、緩和効果が初期から現れるという特異な挙動を示している。また、NRF-SAT は非精緻化抽象化（non-refined abstractions）によって数式の巨大化を緩和できるため、SMT-CBS よりも UA の影響を受けにくい高い効率性を示している。
本研究では、割り当てられないエージェントが存在するマルチエージェント経路探索（UA-MAPF）のバリアントを調査し、既存のSATベースのソルバーである SMT-CBS および NRF-SAT を UA-MAPF へ適応させる手法を提案している。適応にあたっては、MDD（Multi-valued Decision Diagram）の代わりに UA-MDD を生成するように構成を変更するだけで済み、SATベースの手法のモジュール性と適応性の高さが示された。実験評価の結果、大規模なマップにおいては、割り当てられないエージェントの数が増えることが問題の緩和につながるという直感に反して、実行時間が長くなるという傾向が確認されたが、最終的にはエージェントの過半数が割り当てられない状態になると緩和の効果が上回る。今後の展望として、連続的な空間における MAPF 問題への UA-MAPF の導入が挙げられている。