Unifying Search-based and Compilation-based Approaches to
Multi-agent Path Finding through Satisfiability Modulo Theories
Abstract
We unify search-based and compilation-based approaches to multi-agent path finding (MAPF)
through satisfiability modulo theories (SMT). The
task in MAPF is to navigate agents in an undirected
graph to given goal vertices so that they do not collide. We rephrase Conflict-Based Search (CBS),
one of the state-of-the-art algorithms for optimal
MAPF solving, in the terms of SMT. This idea
combines SAT-based solving known from MDDSAT, a SAT-based optimal MAPF solver, at the
low-level with conflict elimination of CBS at the
high-level. Where the standard CBS branches the
search after a conflict, we refine the propositional
model with a disjunctive constraint. Our novel algorithm called SMT-CBS hence does not branch at
the high-level but incrementally extends the propositional model. We experimentally compare SMTCBS with CBS, ICBS, and MDD-SAT.