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

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.