Learn all about Multi-Agent Path Finding (MAPF)

P. Surynek. On Satisfisfiability Modulo Theories in Continuous Multi-Agent Path Finding: Compilation-Based and Search-Based Approaches Compared. In* Proceedings of the International Conference on Agents and Artificial Intelligence (ICAART),* pages 182-193, 2020.

Abstract: Multi-agent path finding (MAPF) in continuous space and time with geometric
agents, i.e. agents of various geometric shapes moving smoothly between
predefined positions, is addressed in this paper. We analyze a new solving
approach based on satisfiability modulo theories (SMT) that is designed to
obtain makespan optimal solutions. The standard MAPF is a task of navigating
agents in an undirected graph from given starting vertices to given goal
vertices so that agents do not collide with each other in vertices or edges of
the graph. In the continuous version (MAPF^{R}), agents move in an
$n$-dimensional Euclidean space along straight lines that interconnect
predefined positions. Agents themselves are geometric objects of various
shapes occupying certain volume of the space - circles, polygons, etc. For
simplicity, we work with circular omni-directional agents having constant
velocities in the 2D plane. As agents can have different shapes/sizes and are
moving smoothly along lines, a movement along certain lines done with small
agents can be non-colliding while the same movement may result in a collision
if performed with larger agents. Such a distinction rooted in the geometric
reasoning is not present in the standard MAPF. The SMT-based approach for
MAPF^{R} reformulates the well established
Conflict-based Search (CBS) algorithm in terms of SMT. Lazy generation of
decision variables and constraints is the key idea behind SMT-CBS. Each time a
new conflict is discovered, the underlying encoding is extended with new
variables and constraints to eliminate the conflict. We compared
SMT-CBS^{R} and adaptations of CBS for the continuous variant of MAPF
experimentally.