基于 SMT 的动态多机器人任务分配

多机器人任务分配（MRTA）是许多应用领域中存在的问题，包括包裹配送、仓储机器人和医疗保健。在本工作中，我们考虑了具有任务截止期限和有容量限制的智能体（可同时执行多个任务的容量）的动态任务流 MRTA 问题。以往的工作通常关注静态情形，针对限制性任务规范使用专用算法，或者缺乏保证。我们提出了一种基于可满足性模理论（SMT）求解的、面向有容量限制机器人的动态 MRTA 方法，并解决了这些问题。我们证明了我们的方法既是可靠的又是完备的，且 SMT 编码具有通用性，能够扩展到更广泛的任务规范类别。我们展示了如何利用 SMT 求解器的增量求解能力，在分配在线到达的新任务时保留已学习的信息，以及如何进行非增量求解，并提供了两者的运行时间比较。此外，我们提供了一种算法，从较小但可能不完备的编码开始，可以迭代地调整至完备编码。我们在一组参数化的基准测试上评估了我们的方法，这些基准测试编码了由类医院环境的图抽象创建的多机器人配送任务。我们使用一系列编码展示了我们方法的有效性，包括在多个求解器上使用无解释函数的无量词理论和线性或位向量算术。