Unifying Search-Based and Compilation-Based Approaches to Multi-Agent Path Finding through Satisfiability Modulo Theories
Unifying Search-Based and Compilation-Based Approaches to Multi-Agent Path Finding through Satisfiability Modulo Theories
复制标题
通过可满足性模理论统一基于搜索和基于编译的多代理路径查找方法
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Pavel Surynek
中科院分区：
文献类型：
--
作者：
Pavel Surynek
我们通过可满足模理论（SMT）统一了基于搜索和基于编译的多智能体路径查找（MAPF）方法。MAPF的任务是将无向图中的代理导航到给定的目标顶点，使它们不发生碰撞。我们将基于冲突的搜索（CBS）作为最优MAPF求解的最先进算法之一，重新定义为SMT。这个想法结合了MDD-SAT（一种基于sat的最优MAPF求解器）的基于sat的解决方案，在底层与在高层消除CBS的冲突。在标准CBS对冲突后的搜索进行分支的地方，我们使用析取约束来改进命题模型。因此，我们的新算法称为SMT-CBS，不会在高层进行分支，而是逐步扩展命题模型。我们通过实验比较了SMT-CBS与CBS、ICBS和MDD-SAT。
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 MDD-SAT, 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 SMT-CBS with CBS, ICBS, and MDD-SAT.