Lazy Compilation of Variants of Multi-robot Path Planning with Satisfiability Modulo Theory (SMT) Approach

摘要

We address variants of multi-robot path planning in graphs (MRPP). We assume robots placed in vertices of an undirected graph with at most one robot per vertex. Robots can move across edges while various problem specific constraints must be satisfied. We introduce a general problem formulation that encompasses known types of robot relocation problems such as multi-robot path planning (MRPP), token swapping (TSWAP), token rotation (TROT), and token permutation (TPERM). We generalize SMT-CBS, a recent solving approach for MRPP based on satisfiability modulo theories (SMT). SMT- CBS compiles MRPP lazily within the SMT framework, starting with the basic model that is refined with a collision resolution constraints whenever collisions between robots occur in the current solution. We show modifications the SMT-CBS algorithm for variants of MRPP and evaluate them experimentally.