An SMT-Based Approach to Motion Planning for Multiple Robots With Complex Constraints

In this paper, we propose a new method for solving multirobot motion planning problems with complex constraints. We focus on an important class of problems that require an allocation of spatially distributed tasks to robots, along with efficient paths for each robot to visits their task locations. We introduce a framework for solving these problems that naturally couples allocation with path planning. The allocation problem is encoded as a Boolean Satisfiability problem (SAT) and the path planning problem is encoded as a traveling salesman problem (TSP). In addition, the framework can handle complex constraints such as battery life limitations, robot carrying capacities, and robot-task incompatibilities. We propose an algorithm that leverages recent advances in Satisfiability Modulo Theory (SMT) to combine state-of-the-art SAT and TSP solvers. We characterize the correctness of our algorithm and evaluate it in simulation on a series of patrolling, periodic routing, and multirobot sample collection problems. The results show our algorithm significantly outperforms state-of-the-art mathematical programming solvers.