Publication

P. Surynek. On Satisfiability 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), 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 called SMT-CBS-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.

Download the paper in pdf.