  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.
