基于非精化抽象的反例引导抽象精化在多智能体路径规划中的应用
人工智能
2023-01-23 v1
摘要
反例引导抽象精化（CEGAR）是一种用于模型检测与可达性分析等多种任务的强大符号技术。近来，CEGAR 与布尔可满足性（SAT）相结合被应用于多智能体路径规划（MAPF），该问题要求将智能体从其起始位置导航至给定的各自目标位置，且智能体之间不发生碰撞。近期的 CEGAR 方法使用了 MAPF 问题的初始抽象，其中智能体间的碰撞被忽略，并在后续抽象精化中被消除。我们在本工作中提出一种基于 SAT 的新型 CEGAR 风格 MAPF 求解器，其中某些抽象被有意保留为非精化状态。这增加了对底层 SAT 求解器所得答案进行后处理的必要性，因为这些答案与正确的 MAPF 解略有差异。然而，非精化产生的 SAT 编码比先前方法小一个数量级，并加速了整体求解过程，使基于 SAT 的 MAPF 求解器在相关基准中重新具备竞争力。
引用
@article{arxiv.2301.08687,
title = {Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Agent Path Finding},
author = {Pavel Surynek},
journal= {arXiv preprint arXiv:2301.08687},
year = {2023}
}