Victoria Tuck, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S. Shankar Sastry and Sanjit A. Seshia
EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2024-12
March 18, 2024
http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-12.pdf
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.
BibTeX citation:
@techreport{Tuck:EECS-2024-12,
Author = {Tuck, Victoria and Chen, Pei-Wei and Fainekos, Georgios and Hoxha, Bardh and Okamoto, Hideki and Sastry, S. Shankar and Seshia, Sanjit A.},
Title = {SMT-Based Dynamic Multi-Robot Task Allocation},
Institution = {EECS Department, University of California, Berkeley},
Year = {2024},
Month = {Mar},
URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-12.html},
Number = {UCB/EECS-2024-12},
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.}
}
EndNote citation:
%0 Report %A Tuck, Victoria %A Chen, Pei-Wei %A Fainekos, Georgios %A Hoxha, Bardh %A Okamoto, Hideki %A Sastry, S. Shankar %A Seshia, Sanjit A. %T SMT-Based Dynamic Multi-Robot Task Allocation %I EECS Department, University of California, Berkeley %D 2024 %8 March 18 %@ UCB/EECS-2024-12 %U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2024/EECS-2024-12.html %F Tuck:EECS-2024-12