  Layout synthesis is mapping a quantum circuit to a quantum processor. SWAP
gate insertions are needed for scheduling 2-qubit gates only on connected
physical qubits. With the ever-increasing number of qubits in NISQ processors,
scalable layout synthesis is of utmost importance. With large optimality gaps
observed in heuristic approaches, scalable exact methods are needed. While
recent exact and near-optimal approaches scale to moderate circuits, large deep
circuits are still out of scope.
  In this work, we propose a SAT encoding based on parallel plans that apply 1
SWAP and a group of CNOTs at each time step. Using domain-specific information,
we maintain optimality in parallel plans while scaling to large and deep
circuits. From our results, we show the scalability of our approach which
significantly outperforms leading exact and near-optimal approaches (up to
100x). For the first time, we can optimally map several 8, 14, and 16 qubit
circuits onto 54, 80, and 127 qubit platforms with up to 17 SWAPs. While adding
optimal SWAPs, we also report near-optimal depth in our mapped circuits.
