This paper introduces a new approach to solving a continuous-time version of the multi-agent path finding problem. The algorithm translates the problem into an extension of the classical Boolean satisfiability problem, satisfiability modulo theories (SMT), that can be solved by off-the-shelf solvers. This enables the exploitation of conflict generalization techniques that such solvers can handle. Computational experiments show that the new approach scales better with respect to the available computation time than state-of-the art approaches and is usually able to avoid their exponential behavior on a class of benchmark problems modeling a typical bottleneck situation.

翻译：本文提出了一种解决连续时间多智能体路径规划问题的新方法。该算法将该问题转化为经典布尔可满足性问题（可满足性模理论，SMT）的扩展形式，可通过现成的求解器进行求解。这种方法使得能够利用此类求解器可处理的冲突泛化技术。计算实验表明，与现有最优方法相比，新方法在可用计算时间上的扩展性更优，并且通常能够避免在模拟典型瓶颈情形的一类基准问题上出现的指数级行为。