Qubit Mapping and Routing via MaxSAT

Near-term quantum computers will operate in a noisy environment, without error correction. A critical problem for near-term quantum computing is laying out a logical circuit onto a physical device with limited connectivity between qubits. This is known as qubit mapping and routing (QMR), an intractable combinatorial problem. It is important to solve QMR as optimally as possible to reduce the amount of added noise, which may render a quantum computation useless. In this work, we develop a novel approach for optimally solving the QMR problem via a reduction to the maximum satisfiability problem (MAXSAT). Additionally, we present two novel relaxation ideas that shrink the size of the MAXSAT constraints by exploiting the structure of a quantum circuit. The first relaxation slices the circuit horizontally into a number of consecutive subcircuits and solves a set of smaller MAXSAT problems for each of them. The second relaxation allows for efficient mapping of cyclic circuits, like in quantum approximate optimization algorithms (QAOA). Cyclic circuits are those where the same subcircuit is repeated more than once. Instead of generating one large set of constraints for the entire circuit, we solve a special set of MAXSAT constraints only for the repeated subcircuit in isolation, and then stitch the subcircuits back together to generate a mapping for the entire circuit. Our thorough empirical evaluation demonstrates (1) the scalability of our approach compared to state-of-the-art optimal QMR techniques, (2) the significant cost reduction compared to state-of-the-art heuristic approaches, and (3) the power of our proposed constraint relaxations.