迈向 DPLL(MAPF) 及更远的探索之路

我们讨论了迈向 DPLL(MAPF) 这一里程碑式的工作，DPLL(MAPF) 是一个通过可满足性模理论（SMT）与 Davis-Putnam-Logemann-Loveland（DPLL）命题可满足性测试算法完全集成的多智能体路径规划（MAPF）求解器。MAPF 的任务是在无向图中以无碰撞的方式引导智能体，使每个智能体最终到达其唯一目标顶点。任一时刻至多一个智能体可占据一个顶点。智能体可通过遍历边瞬时移动，只要该移动不会导致碰撞。近来，基于将 MAPF 归约为命题可满足性（SAT）来最优地求解关于代价和或完工时间的 MAPF 的尝试已经出现。最成功的方法依赖于受 SMT 范式启发的流程，惰性地为给定 MAPF 实例构建命题编码。然而，在现有方法中，SAT 求解器的可满足性测试与编码的高层构建之间的集成相对松散。因此，该方向研究的终极目标是构建 DPLL(MAPF) 算法，一种将编码构建与底层 SAT 求解器完全集成的 MAPF 求解器。我们讨论了 MAPF 求解的当前最先进水平，以及为获得 DPLL(MAPF) 所需完成的步骤。还讨论了 DPLL(MAPF) 的潜在优势，即其可被 MAPF$^R$（一种具有几何智能体的连续 MAPF 理论）替代参数化的潜力。