Abstract
This paper addresses makespan optimal solving of cooperative path-finding problem (CPF) by translating it to propositional satisfiability (SAT). The task in CPF is to relocate a set of agents to given goal locations so that they do not collide with each other.
Recent findings indicate that a simple direct en-coding outperforms the more elaborate encodings based on binary encodings of multi-value state variables. The direct encoding is further improved by a hierar-chical build-up that uses auxiliary variables to reduce its size in this work.
The conducted experimental evaluation shown that the simple design of the encod-ing together with new improvements which reduced its size significantly are key enablers for faster solving of the encoded CPFs than with existing encod-ings. It has been also shown that the SAT based methods dominates over A* based methods in environments with high occupancy by agents.