An SAT-based approach to cooperative path-finding using all-different constraints

Abstract

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. Copyright © 2012, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.