  Practical applications of quantum computing depend on fault-tolerant devices
with error correction. Today, the most promising approach is a class of
error-correcting codes called surface codes. In this paper, we study the
problem of compiling quantum circuits for quantum computers implementing
surface codes. The problem involves (1) mapping circuit qubits to the device
qubits and (2) routing execution paths between pairs of interacting qubits. We
call this the surface code mapping and routing problem (SCMR).
  Solving SCMR near-optimally is critical for both efficiency and correctness.
An optimal solution limits the cost of a computation in terms of precious
quantum resources and also minimizes the probability of incurring an undetected
logical error, which increases with each additional time step.
  We study SCMR from a theoretical and practical perspective. First, we prove
that SCMR, as well as a constrained version of the problem, is NP-complete.
Second, we present a optimal algorithm for solving SCMR that is based on a SAT
encoding. Third, we present a spectrum of efficient relaxations of SCMR, for
example, by exploiting greedy algorithms for solving the problem of
node-disjoint paths. Finally, we implement and evaluate our algorithms on a
large suite of real and synthetic circuits. Our results suggest that our
relaxations are a powerful tool for compiling realistic workloads. The
relaxation-based algorithms are orders of magnitude faster than the optimal
algorithm (solving instances with tens of thousands of gates in minutes), while
still finding high-quality solutions, achieving the theoretical lower bound on
up to 55 out of 168 circuits from a diverse benchmark suite.
