Compilation-based techniques represent an important stream of solvers for multi-agent path finding (MAPF) due to their modularity and adaptability for non-standard variants of the problem. While in the standard MAPF the task is to navigate all agents from their initial positions to given individual goal positions without any collision, variants where a different requirement for agents is used are also relevant. Such a variant is MAPF with unassigned agents (UA-MAPF) where some agents have the same setting as in the standard MAPF with initial positions and goals while the remaining agents have the initial position but have no goal - unassigned agents. Despite unassigned agent do not need to reach any goal position they have to be moved out of the way of the standard agents if needed which represent a specific challenge. We show in this paper that UA-MAPF can be expressed in recent compilation-based techniques for MAPF based on formulating the problem as Boolean satisfiability, namely we adapt SMT-CBS and NRF-SAT, the recent solvers based on counterexample guided abstraction refinement and non-refined abstractions.

翻译：基于编译的技术因其模块化及对非标准变体问题的适应性，成为多智能体路径规划（MAPF）求解器的重要分支。在标准MAPF中，任务是引导所有智能体从初始位置移动至指定的独立目标位置且无任何碰撞，但采用不同智能体要求的变体同样具有研究价值。其中一类变体为含未分配智能体的MAPF（UA-MAPF）：部分智能体与标准MAPF设置相同（具备初始位置与目标），而其余智能体仅具有初始位置但无目标——即未分配智能体。尽管未分配智能体无需抵达任何目标位置，但在必要时需为常规智能体让路，这构成了特殊挑战。本文证明，UA-MAPF可借助最新基于编译的MAPF技术（通过将问题表述为布尔可满足性）进行表示。具体而言，我们改进了基于反例引导抽象精化与非精化抽象的最新求解器SMT-CBS与NRF-SAT。