This chapter summarizes the contributions of Part III of this book, which explores the challenge of determining optimal solutions to the quantum circuit mapping problem. The proposed solutions encode the respective problem in a symbolic fashion and use powerful reasoning engines to cope with the vast complexity of the underlying problem. The resulting methods have been integrated into the open-source quantum circuit compilation tool MQT QMAP, which is available at https://github.com/munich-quantum-toolkit/qmap .