Counterexample guided abstraction refinement (CEGAR) represents a powerful symbolic technique for various tasks such as model checking and reachability analysis. Recently, CEGAR combined with Boolean satisfiability (SAT) has been applied for multi-agent path finding (MAPF), a problem where the task is to navigate agents from their start positions to given individual goal positions so that the agents do not collide with each other. The recent CEGAR approach used the initial abstraction of the MAPF problem where collisions between agents were omitted and were eliminated in subsequent abstraction refinements. We propose in this work a novel CEGAR-style solver for MAPF based on SAT in which some abstractions are deliberately left non-refined. This adds the necessity to post-process the answers obtained from the underlying SAT solver as these answers slightly differ from the correct MAPF solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous approach and speeds up the overall solving process making the SAT-based solver for MAPF competitive again in relevant benchmarks.
翻译:反相引导抽象精炼(CEGAR)是模型检查和可达性分析等各种任务的一种强有力的象征性技术。最近,CEGAR与Boolean可探测性(SAT)结合应用于多试剂路径发现(MAPF),这是一个任务在于将试剂从最初位置导航到给定单个目标位置,从而使试剂不会相互碰撞的问题。最近,CEGAR方法使用了MAPF问题的初步抽象方法,其中排除了各种物剂之间的碰撞,并在随后的抽象改进中予以消除。我们在此工作中为MAPF提出了基于SAT的新型CEGAR型解析器,其中某些抽象内容被有意地保留在未修。这增加了从基本SAT求解答器获得的答案与正确的MAPF解决方案略有不同的后处理过程的必要性。尽管这些解答方法与先前方法相比产生微微的SAT编码,但降出比先前方法小的卫星编码的速度加快了总体解算过程,使基于SAT的解算器在相关基准中再次具有竞争力。