Publication

J. Svancara, R. Bartak, I. Miguel and J. Espasa. Modelling Multi-Agent Pathfinding Problems by Integrating Connectivity and No-Collision Constraints. In International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 3686-3694, 2026.

Abstract: Multi-agent pathfinding (MAPF) is the problem of finding collision- free paths for a set of agents in a shared environment, typically represented as a graph. One of the approaches to solving MAPF is based on representing the problem as a Boolean satisfiability prob- lem. However, this method can produce extremely large Boolean formulas, both in terms of variables and clauses. The primary rea- son for the excessive number of clauses is the encoding required to represent the valid paths. In this paper, we propose two en- codings of the MAPF problem designed for SAT Modulo Theories solvers. Our approach delegates all the valid path reasoning to a monotonic theory supporting source-target connectivity. This is then combined with a 2-SAT Boolean formula to prevent collisions between agents. Together, these components create an effective sep- aration of concerns: the SAT solver focuses on resolving conflicts, while the theory solver handles the connectivity constraints. Our experiments are conducted in both makespan and sum of costs opti- misation settings, empirically demonstrating a notable reduction in both the size of the MAPF encoding and the time required to gener- ate it. In addition, when fixing the SAT solver across experiments, results demonstrate considerable performance improvements when transitioning from pure SAT to our proposed SMT encodings.

Download the paper in pdf.