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


  • Pavel Surynek Czech Technical University in Prague, Faculty of Information Technology


Continuous Problem Solving, Problem Compilation, Search In Boolean Satisfiability, Search Space Discretization For Continuous State-space Problems


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.