This chapter presents an optimal quantum circuit mapping technique based on a symbolic formulation that encodes the whole search space of the mapping problem. To tackle the inherent complexity, sophisticated reasoning engines, such as Boolean satisfiability solvers, are used that are capable of handling huge search spaces. Additionally, performance optimizations are proposed that can generate solutions that are not always minimal but can greatly reduce the solving time while still producing near-optimal results. Experimental evaluations have shown that at time [3] was published, IBM Qiskit’s heuristic solution exceeded the lower bound by more than 100% on average.