Main /
PublicationP. Surynek. On Satisfiability Modulo Theories in Continuous MultiAgent Path Finding: CompilationBased and SearchBased Approaches Compared. In Proceedings of the International Conference on Agents and Artificial Intelligence (ICAART), 2020. Abstract: Multiagent 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 (MAPFR), agents move in an ndimensional 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 omnidirectional 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 noncolliding 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 SMTbased approach for MAPFR called SMTCBSR reformulates the well established Conflictbased Search (CBS) algorithm in terms of SMT. Lazy generation of decision variables and constraints is the key idea behind SMTCBS. Each time a new conflict is discovered, the underlying encoding is extended with new variables and constraints to eliminate the conflict.We compared SMTCBSR and adaptations of CBS for the continuous variant of MAPF experimentally.
