Pushing the Envelope: From Discrete to Continuous Movements in Multi-Agent Path Finding via Lazy Encodings
This work addresses path planning for multiple agents in continuous environments, which is crucial for robotics and autonomous systems, representing an incremental improvement over existing methods.
The paper tackles the problem of multi-agent path finding in continuous space and time with geometric agents (MAPF^R), introducing SMT-CBS^R, a novel algorithm that combines conflict-based search with satisfiability modulo theories to achieve makespan optimal solutions, and experimentally shows it outperforms the previous CCBS algorithm.
Multi-agent path finding in continuous space and time with geometric agents MAPF$^\mathcal{R}$ is addressed in this paper. The task is to navigate agents that move smoothly between predefined positions to their individual goals so that they do not collide. We introduce a novel solving approach for obtaining makespan optimal solutions called SMT-CBS$^\mathcal{R}$ based on {\em satisfiability modulo theories} (SMT). The new algorithm combines collision resolution known from conflict-based search (CBS) with previous generation of incomplete SAT encodings on top of a novel scheme for selecting decision variables in a potentially uncountable search space. We experimentally compare SMT-CBS$^\mathcal{R}$ and previous CCBS algorithm for MAPF$^\mathcal{R}$.