Mutex Propagation for SAT-based Multi-Agent Path Finding

Abstract

Multi-agent path finding (MAPF) is the problem of planning a set of non-colliding paths for a set of agents so that each agent reaches its individual goal location following its path. A mutex from classical planning is a constraint forbidding a pair of facts to be both true or a pair of actions to be executed simultaneously. In the context of MAPF, mutexes are used to rule out the simultaneous occurrence of a pair of agents in a pair of locations, which can prune the search space. Previously mutex propagation had been integrated into conflict-based search (CBS), a major search-based approach for solving MAPF optimally. In this paper, we introduce mutex propagation into the compilation-based (SAT-based) solver MDD-SAT, an alternative to search-based solvers. Our experiments show that, despite mutex propagation being computationally expensive, it prunes the search space significantly so that the overall performance of MDD-SAT is improved.