Publication at Faculty of Mathematics and Physics |
2014
Abstract
This paper addresses makespan optimal solving of cooperative path-finding problem (CPF) by translating it to propositional satisfiability (SAT). The task is to relocate set of agents to given goal positions so that they do not collide with each other.
A novel SAT encoding of CPF is suggested. The novel encoding uses the concept of matching in a bipartite graph to separate spatial constraint of CPF from consideration of individual agents.
The separation allowed reducing the size of encoding significantly. The conducted experimental evalua-tion shown that novel encoding can be solved faster than exist-ing encodings for CPF and also that the SAT based methods dominates over A* based methods in environment densely occupied by agents.