Multi-Robot Task Allocation (MRTA) is a problem that arises in many application domains including package delivery, warehouse robotics, and healthcare. In this work, we consider the problem of MRTA for a dynamic stream of tasks with task deadlines and capacitated agents (capacity for more than one simultaneous task). Previous work commonly focuses on the static case, uses specialized algorithms for restrictive task specifications, or lacks guarantees. We propose an approach to Dynamic MRTA for capacitated robots that is based on Satisfiability Modulo Theories (SMT) solving and addresses these concerns. We show our approach is both sound and complete, and that the SMT encoding is general, enabling extension to a broader class of task specifications. We show how to leverage the incremental solving capabilities of SMT solvers, keeping learned information when allocating new tasks arriving online, and to solve non-incrementally, which we provide runtime comparisons of. Additionally, we provide an algorithm to start with a smaller but potentially incomplete encoding that can iteratively be adjusted to the complete encoding. We evaluate our method on a parameterized set of benchmarks encoding multi-robot delivery created from a graph abstraction of a hospital-like environment. The effectiveness of our approach is demonstrated using a range of encodings, including quantifier-free theories of uninterpreted functions and linear or bitvector arithmetic across multiple solvers.

翻译：多机器人任务分配（MRTA）是出现在包裹递送、仓储机器人及医疗保健等多个应用领域的问题。本文针对具有任务截止时间与容量受限智能体（可同时执行多项任务）的动态任务流，研究MRTA问题。以往研究通常聚焦静态场景，针对限制性任务规范使用专用算法，或缺乏保证机制。我们提出一种基于可满足性模理论（SMT）求解的容量受限机器人动态MRTA方法，解决了上述问题。研究表明该方法兼具完备性和正确性，且SMT编码具有通用性，可扩展至更广泛的任务规范类别。我们展示了如何利用SMT求解器的增量求解能力（在实时分配新任务时保留已学习信息）和非增量求解能力，并提供了两者的运行时间对比。此外，我们提出一种从较小但可能不完整的编码开始，通过迭代调整达到完整编码的算法。我们在基于医院环境图抽象构建的参数化多机器人递送基准集上评估该方法。通过包括无量纲解释函数理论、线性或位向量算术在内的多种求解器编码，验证了该方法的有效性。