  Trapped ions are a promising technology for building scalable quantum
computers. Not only can they provide a high qubit quality, but they also enable
modular architectures, referred to as Quantum Charge Coupled Device (QCCD)
architecture. Within these devices, ions can be shuttled (moved) throughout the
trap and through different dedicated zones, e.g., a memory zone for storage and
a processing zone for the actual computation. However, this movement incurs a
cost in terms of required time steps, which increases the probability of
decoherence, and, thus, should be minimized. In this paper, we propose a
formalization of the possible movements in ion traps via Boolean
satisfiability. This formalization allows for determining the minimal number of
time steps needed for a given quantum algorithm and device architecture, hence
reducing the decoherence probability. An empirical evaluation confirms that --
using the proposed approach -- minimal results (i.e., the lower bound) can be
determined for the first time. An open-source implementation of the proposed
approach is publicly available at https://github.com/cda-tum/mqt-ion-shuttler.
