Ghost Agents in SAT-based Models for Multi-Agent Pathfinding

Abstract

Multi-agent pathfinding (MAPF) is the task of navigating a set of mobile agents in a shared environment while avoiding collisions when multiple agents occupy the same space simultaneously. One popular approach to solving MAPF is to transform the problem into a different formalism, such as Boolean satisfiability (SAT), and solve the problem using an off-the-shelf SAT solver. The current state-of-the-art SAT-based MAPF solvers model the position of each agent at each timestep as a Boolean variable and enforce valid movement and coordination via constraints among those variables encoded as a logical formula. It might be expected that the formula encodes a single valid, collision-free path for each agent, meaning that at any given time, each agent occupies exactly one location. In this paper, we explore the possibility of an agent being present at multiple locations simultaneously. While such relaxed encoding exists in the literature, the presence of duplicate agents is not discussed. In this paper, we coin the term ghost agents and show that their presence does not hinder the validity of the solution. As the relaxed encoding reduces the size of the formula, we compare it empirically. Furthermore, we compare empirically all approaches used in reduction-based MAPF solving and their combinations: single and ghost agents, with eager and lazy encodings of conflicts under both the makespan and the sum-of-costs objectives. The experiments show that no combination is a clear winner in all types of instances.