Multi-Agent Path Finding with Continuous Time Using SAT Modulo Linear Arithmetic Over the Reals
摘要
We introduce a new approach to solving a continuous-time version of the multi-agent path finding problem. The approach is based on an extension of the classical Boolean satisfiability problem, satisfiability modulo theories (SMT), more specifically, satisfiability modulo linear arithmetic over the reals (SMT(LRA)). The algorithm iteratively improves an approximation of the path finding problem by predicate logical formulas in the language of SMT(LRA). It solves these formulas using off-the-shelf solvers, which enables the exploitation of powerful conflict generalization techniques. Computational experiments show that the new approach scales better with respect to the available computation time than state-of-the-art approaches. Moreover, it is often able to avoid their exponential behavior in bottleneck situations. On the downside, the problem encoding into logical formulas needs a certain computational overhead that may dominate in the case of problems modeled by large graphs.