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.

The research at the Czech Technical University in Prague was supported by GAČR - the Czech Science Foundation, under grant number 19-17966S. The research at the University of Southern California was supported by National Science Foundation (NSF) under grant numbers 1409987, 1724392, 1817189, 1837779, and 1935712 as well as a gift from Amazon.