Modelling Multi-Agent Pathfinding Problems by Integrating Connectivity and No-Collision Constraints (Extended Abstract)

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 problem. However, this method can produce extremely large Boolean formulas, both in terms of variables and clauses. The primary reason for the excessive number of clauses is the encoding required to represent the valid paths. In this paper, we propose two encodings 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 separation 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 optimisation settings, empirically demonstrating a notable reduction in both the size of the MAPF encoding and the time required to generate 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.