SMT-Based Dynamic Multi-Robot Task Allocation

TL;DR

This work proposes an approach to Dynamic MRTA for capacitated robots that is based on Satisfiability Modulo Theories (SMT) solving and shows how to leverage the incremental solving capabilities of SMT solvers, keeping learned information when allocating new tasks arriving online, and to solve non-incrementally.

Abstract

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.

Figures (6)

• Figure 1: A task stream of sets of tasks arrives with monotonically increasing arrival times. Five system sites are shown. Example tasks and robot paths are shown on the right with $P$, $D$, and $M$ used to represent the actions succinctly. The result action sequence for the right robot is (M,P,M,D) and (M,P,M,P,M,P,M,D,M,D,M,D). The moves between picks or drops at the same location are used to keep a consistent structure in the plan but take no time.
• Figure 2: Constraints used in the encoding developed in Algorithm \ref{['alg:overall']}
• Figure 3: Flow chart of Algorithm \ref{['alg:overall']} starting at the black circle. $A \ \slash \ B$ denotes a conditional $A$ and a changed variable $B$. On the right is the assumption block to manage problem size. The third row from the top (in yellow) shows pushes and pops of the solver state.
• Figure 4: Cactus plot for solver runtimes. Red line represents the 3600s timeout.
• Figure 5: Runtime analysis on Bitwuzla-BV and Z3-BV under multiple settings. Boxes represent quantiles, circles represent outliers, and lines represent means of runtimes. Observe that runtimes are faster when number of agents is larger.

Theorems & Definitions (37)

• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition
• definition thmcounterdefinition