Mutex reasoning in cooperative path finding modeled as propositional satisfiability

This paper addresses a problem of cooperative path finding (CPF) where the task is to find paths for agents of a group of agents. Each agent is given a starting and a goal position and its task is to reach the goal from the given start. When following the paths, agents must not collide with each other and must avoid obstacles. It is suggested to augment propositional encodings of CPF with a so called mutex reasoning. Mutex reasoning is trying to rule out unreachable situations to reduce the size of the search space. It is checked whether a given pair of locations is reachable by a given pair of agents cooperatively. If not occurrence of the pair of agents in the pair of vertices is forbidden. The performed experimental evaluation showed that mutex reasoning improves existent encodings by 2 to 5 times in terms of solving runtime when makespan optimal solutions are searched.