A SAT-Based Approach to Cooperative Path-Finding Using All-Different Constraints

Proceedings of the International Symposium on Combinatorial Search, 5

Volume

Vol. 5 No. 1 (2012): Fifth Annual Symposium on Combinatorial Search

Extended Abstracts of Papers Presented Elsewhere

The approach to solving cooperative-path finding (CPF) as satisfiability (SAT) is revisited. An alternative encoding that exploits multi-valued state variables representing locations where a given agent resides is suggested. This encoding employs the ALL-DIFFERENT constraint to model the requirement that agents must not collide with each other. We show that our new domain-dependent encoding enables finding of optimal or near optimal solutions to CPFs in certain hard setups where A*-based techniques such as WHCA* fail to do so. Our finding is also that the ALL-DIFFERENT encoding can be solved faster than the existent encoding.

10.1609/socs.v3i1.18220