2023/12/13 by Tomáš Kolárik, Kolárik, Tomáš, Stefan Ratschan +3
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Metaheuristic Optimization Algorithms Research #Multiagent Systems (cs.MA) #Robotic Path Planning Algorithms
paper · pdf · doi:10.48550/arxiv.2312.08051
openalex publication_date 2023/12/13 · openalex created_date 2023/12/15 · openalex updated_date 2026/07/28
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.