Compact Representations of Cooperative Path-Finding as SAT Based on Matchings in Bipartite Graphs. Surynek, P. In Proceedings of the 26th International Conference on Tools with Artificial Intelligence (ICTAI), pages 875–882, 2014.
abstract   bibtex   
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 evaluation shown that novel encoding can be solved faster than existing encodings for CPF and also that the SAT based methods dominates over A* based methods in environment densely occupied by agents.
@INPROCEEDINGS{PSury14a, 
 AUTHOR= "P. Surynek",
 TITLE= "Compact Representations of Cooperative Path-Finding as {SAT} Based on Matchings in Bipartite Graphs",
 BOOKTITLE= "Proceedings of the 26th International Conference on Tools with Artificial Intelligence (ICTAI)",
 PAGES= "875--882",
 YEAR= "2014",
 PDF= "http://surynek.com/publications/files/SurynekPavel_Matching-Code_ICTAI-2014.pdf",
 FLAGS= ":2014:,:pavelsurynek:",
 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 evaluation shown that novel encoding can be solved faster than
existing encodings for CPF and also that the SAT based methods dominates over
A* based methods in environment densely occupied by agents."
}

Downloads: 0