Lazy Compilation of Variants of Multi-robot Path Planning with Satisfiability Modulo Theory (SMT) Approach
Lazy Compilation of Variants of Multi-robot Path Planning with Satisfiability Modulo Theory (SMT) Approach
复制标题
采用可满足性模理论 (SMT) 方法的多机器人路径规划变体的延迟编译
DOI：
10.1109/iros40897.2019.8967962
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Pavel Surynek
中科院分区：
文献类型：
--
作者：
Pavel Surynek
我们解决多机器人路径规划图（MRPP）的变种。我们假设机器人放置在一个无向图的顶点，每个顶点最多有一个机器人。机器人可以在边缘上移动，同时必须满足各种特定问题的约束。我们介绍了一个一般的问题制定，包括已知类型的机器人重新定位问题，如多机器人路径规划（MRPP），令牌交换（TSWAP），令牌旋转（TROT），令牌置换（TPERM）。我们推广SMT-CBS，最近的解决方法MRPP的基础上可满足模理论（SMT）。SMT-CBS在SMT框架内惰性地编译MRPP，从基本模型开始，每当当前解决方案中发生机器人之间的碰撞时，该基本模型都会使用碰撞解决约束进行细化。我们修改SMT-CBS算法的变体MRPP和实验评估。
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.