结合可满足性模理论和基于搜索的令牌交换问题和多智能体路径查找的惰性建模
Lazy Modeling of Variants of Token Swapping Problem and Multi-agent Path Finding through Combination of Satisfiability Modulo Theories and Conflict-based Search
摘要：
本文讨论了图中的项重定位问题。我们假设在无向图的顶点上放置的项目，每个顶点最多有一个项目。物品可以在边缘上移动，同时必须满足各种约束条件，这取决于重新定位问题的类型。我们介绍了一个一般的问题制定，包括已知类型的项目搬迁问题，如多代理路径查找（MAPF）和令牌交换（TSWAP）。在这个公式中，我们表示两种新类型的搬迁问题来自令牌交换，我们称之为令牌旋转（TROT）和令牌置换（TPERM）。我们的解决方案的项目搬迁相结合的可满足性模理论（SMT）与基于冲突的搜索（CBS）。我们在SMT框架中解释CBS，在SMT框架中，我们从基本模型开始，并在当前解决方案中发生项之间的冲突时使用冲突解决约束来细化模型。标准CBS和我们基于SMT的CBS修改（SMT-CBS）之间的关键区别在于，标准CBS分支搜索以解决冲突，而在SMT-CBS中，我们迭代地添加单个析取冲突解决约束。在多个基准测试上的实验结果表明，SMT-CBS算法的性能明显优于标准CBS算法。我们还比较了SMT-CBS与基于SAT的MDD-SAT求解器的修改，该求解器使用项目重新定位的渴望建模，其中所有潜在的冲突都通过约束提前消除。实验表明，SMT-CBS中的懒惰方法产生的约束比MDD-SAT少，也实现了更快的求解运行时间。
英文摘要：
We address item relocation problems in graphs in this paper. We assume items placed in vertices of an undirected graph with at most one item per vertex. Items can be moved across edges while various constraints depending on the type of relocation problem must be satisfied. We introduce a general problem formulation that encompasses known types of item relocation problems such as multi-agent path finding (MAPF) and token swapping (TSWAP). In this formulation we express two new types of relocation problems derived from token swapping that we call token rotation (TROT) and token permutation (TPERM). Our solving approach for item relocation combines satisfiability modulo theory (SMT) with conflict-based search (CBS). We interpret CBS in the SMT framework where we start with the basic model and refine the model with a collision resolution constraint whenever a collision between items occurs in the current solution. The key difference between the standard CBS and our SMT-based modification of CBS (SMT-CBS) is that the standard CBS branches the search to resolve the collision while in SMT-CBS we iteratively add a single disjunctive collision resolution constraint. Experimental evaluation on several benchmarks shows that the SMT-CBS algorithm significantly outperforms the standard CBS. We also compared SMT-CBS with a modification of the SAT-based MDD-SAT solver that uses an eager modeling of item relocation in which all potential collisions are eliminated by constrains in advance. Experiments show that lazy approach in SMT-CBS produce fewer constraint than MDD-SAT and also achieves faster solving run-times.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
