基于可满足性模理论与冲突搜索结合的标记交换问题变体及多智能体路径规划的惰性建模
人工智能
2018-09-18 v1
摘要
本文研究图中的物品重定位问题。假设物品放置于无向图的顶点上，每顶点至多一个物品。物品可沿边移动，同时须满足依赖于重定位问题类型的各种约束。我们引入一种涵盖多智能体路径规划（MAPF）与标记交换（TSWAP）等已知物品重定位问题类型的通用问题表述。在该表述中，我们表达了由标记交换衍生的两类新型重定位问题，称为标记轮换（TROT）与标记置换（TPERM）。我们解决物品重定位的方法将可满足性模理论（SMT）与基于冲突的搜索（CBS）相结合。我们在 SMT 框架中解释 CBS：从基本模型出发，每当当前解中出现物品间冲突便以冲突消解约束精炼模型。标准 CBS 与我们基于 SMT 的 CBS 改进（SMT-CBS）的关键区别在于，标准 CBS 通过分支搜索解决冲突，而 SMT-CBS 迭代添加单一析取冲突消解约束。在多个基准上的实验评估表明，SMT-CBS 显著优于标准 CBS。我们还将 SMT-CBS 与基于 SAT 的 MDD-SAT 求解器改进版比较，后者采用物品重定位的急切建模，即预先以约束消除所有潜在冲突。实验显示，SMT-CBS 中的惰性方法较 MDD-SAT 产生更少约束且求解运行时间更快。
引用
@article{arxiv.1809.05959,
title = {Lazy Modeling of Variants of Token Swapping Problem and Multi-agent Path Finding through Combination of Satisfiability Modulo Theories and Conflict-based Search},
author = {Pavel Surynek},
journal= {arXiv preprint arXiv:1809.05959},
year = {2018}
}