<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Multi-Agent Path Finding with Continuous Time Using SAT Modulo Linear Arithmetic Over the Reals

  • Tomáš Kolárik,
  • Stefan Ratschan,
  • Pavel Surynek

摘要

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.