一篇论文展示了如何让没有任务的智能体给有任务的智能体让路，用上了SMT-CBS和NRF-SAT求解器，思路很清晰。
本文研究多智能体路径规划（MAPF）的一个变种——未分配智能体MAPF（UA-MAPF），其中部分智能体有起点和终点，而另一些智能体只有起点无终点，须为前者让路。作者将UA-MAPF表达为布尔可满足性问题，改编了两种编译式求解器SMT-CBS和NRF-SAT。实验在标准MAPF基准上验证了该方法的有效性。
Unassigned Agents in Compilation-based Multi-agent Path Finding
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.