Efficient SAT Approach to Multi-Agent Path Finding under the Sum of Costs Objective

Abstract

In the multi-agent path finding (MAPF) the task is to find non-conflicting paths for multiple agents. In this paper we present the first SAT-solver for the sum-of-costs variant of MAPF which was previously only solved by search-based methods.

Using both a lower bound on the sum-of-costs and an upper bound on the makespan, we are able to have a reasonable number of variables in our SAT encoding. We then further improve the encoding by borrowing ideas from ICTS, a search-based solver.

Experimental evaluation on several domains showed that there are many scenarios where the new SAT-based method outperforms the best variants of previous sum-of-costs search solvers - the ICTS and ICBS algorithms.

Keywords

• Efficient SAT Approach
• Multi-Agent Path Finding
• Sum Costs Objective