  In many multi-robot applications, mobile worker robots are often engaged in
performing some tasks repetitively by following pre-computed trajectories. As
these robots are battery-powered, they need to get recharged at regular
intervals. We envision that in the future, a few mobile recharger robots will
be employed to supply charge to the energy-deficient worker robots recurrently,
to keep the overall efficiency of the system optimized.In this setup, we need
to find the time instants and locations for the meeting of the worker robots
and recharger robots optimally. We present a Satisfiability Modulo Theory
(SMT)-based approach that captures the activities of the robots in the form of
constraints in a sufficiently long finite-length time window (hypercycle) whose
repetitions provide their perpetual behavior. Our SMT encoding ensures that for
a chosen length of the hypercycle, the total waiting time of the worker robots
due to charge constraints is minimized under certain condition, and close to
optimal when the condition does not hold. Moreover, the recharger robots follow
the most energy-efficient trajectories. We show the efficacy of our approach by
comparing it with another variant of the SMT-based method which is not scalable
but provides an optimal solution globally, and with a greedy algorithm.
