Main /
PublicationP. Surynek. Continuous MultiAgent Path Finding via Satisfiability Modulo Theories (SMT). In Proceedings of the International Conference on Agents and Artificial Intelligence (ICAART), pages 399420, 2020. Revised Selected Papers. Abstract: We address multiagent path finding (MAPF) with continuous movements and geometric agents, i.e. agents of various geometric shapes moving smoothly between predefined positions. We analyze a new solving approach based on satisfiability modulo theories (SMT) that is designed to obtain optimal solutions with respect to common cumulative objectives. 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. We develop concepts for circular omnidirectional agents having constant velocities in the 2D plane but a generalization for different shapes is possible. 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 previous Conflictbased Search (CBS) algorithm in terms of SMT. Lazy generation of constraints is the key idea behind the previous algorithm SMTCBS. Each time a new conflict is discovered, the underlying encoding is extended with new to eliminate the conflict. SMTCBSR significantly extends this idea by generating also the decision variables lazily. Generating variables on demand is needed because in the continuous case the number of possible decision variables is potentially uncountable hence cannot be generated in advance as in the case of SMTCBS. We compared SMTCBSR and adaptations of CBS for the continuous variant of MAPF experimentally.
