SMT-Based Dynamic Multi-Robot Task Allocation

本文讨论了多机器人任务分配（Multi-Robot Task Allocation，MRTA）问题，该问题在许多应用领域中都会出现，包括包裹递送、仓库机器人和医疗保健等领域。本文考虑了具有任务截止时间和容量代理（能同时执行多个任务）的动态任务流MRTA问题。先前的工作通常关注静态情况，使用专门的算法来处理限制性任务规范，或者缺乏保证。我们提出了一种基于Satisfiability Modulo Theories（SMT）求解的动态MRTA方法，解决了这些问题。我们展示了我们的方法既是完备的也是正确的，并且SMT编码是通用的，可扩展到更广泛的任务规范类别。我们展示了如何利用SMT求解器的增量求解能力，在在线分配新任务时保留学习到的信息，并进行非增量求解，我们提供了运行时比较。此外，我们提供了一种算法，可以从较小但可能不完整的编码开始，逐步调整到完整的编码。我们在一个参数化的基准测试集上评估了我们的方法，该测试集编码了一个类似医院环境的图形抽象的多机器人递送任务。我们使用多个求解器的无解释函数和线性或位向量算术的量化器自由理论等多种编码方式来展示我们方法的有效性。

本论文旨在解决动态多机器人任务分配问题（MRTA），其中任务有截止时间，机器人有容量限制，且任务是动态产生的。这个问题在包裹投递、仓库机器人和医疗保健等领域中经常出现。以前的研究通常集中在静态情况下，使用专门的算法来处理限制性任务规范，或缺乏保证。

本论文提出了一种基于Satisfiability Modulo Theories（SMT）求解的动态MRTA方法，解决了上述问题。该方法具有完备性和准确性，并且SMT编码是通用的，可以扩展到更广泛的任务规范类别。此外，论文还提供了一个算法，可以从较小但可能不完整的编码开始，逐步调整到完整的编码。

本论文还提供了如何利用SMT求解器的增量求解能力，当在线分配新任务时保留学习信息，并提供了非增量求解的运行时比较。实验使用了一个基于医院环境的图形抽象创建的参数化的多机器人投递基准集。本论文的方法在多个求解器中使用了不同的编码，包括未解释函数的量词自由理论和线性或位向量算术。

在最近的研究中，也有一些相关的研究在进行，例如“Multi-robot task allocation and scheduling using iterative combinatorial auctions”和“Multi-robot task allocation with temporal and spatial constraints”。