Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Goal Multi-Robot Path Planning

We address the problem of multi-goal multi robot path planning (MG-MRPP) via counterexample guided abstraction refinement (CEGAR) framework. MG-MRPP generalizes the standard discrete multi-robot path planning (MRPP) problem. While the task in MRPP is to navigate robots in an undirected graph from their starting vertices to one individual goal vertex per robot, MG-MRPP assigns each robot multiple goal vertices and the task is to visit each of them at least once. Solving MG-MRPP not only requires finding collision free paths for individual robots but also determining the order of visiting robot's goal vertices so that common objectives like the sum-of-costs are optimized. We use the Boolean satisfiability (SAT) techniques as the underlying paradigm. A specifically novel in this work is the use of non-refined abstractions when formulating the MG-MRPP problem as SAT. While the standard CEGAR approach for MG-MRPP does not encode collision elimination constraints in the initial abstraction and leave them to subsequent refinements. The novel CEGAR approach leaves some abstractions deliberately 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 MG-MRPP solutions. Non-refining however yields order-of-magnitude smaller SAT encodings than those of the previous CEGAR approach and speeds up the overall solving process.