Sum of Costs Optimal Multi-Agent Path Finding with Continuous Time via Satisfiability Modulo Theories

Abstract

Multi-agent path finding with continuous movements and time (denoted MAPF-R) is addressed. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. Recently a novel solving approach for obtaining makespan optimal solutions called SMT-CCBS based on satisfiability modulo theories (SMT) has been introduced. We extend the approach further towards the sum-of-costs objective which is a more challenging case in the yes/no SMT environment due to more complex calculation of the objective.