Quantum computing (QC) is a new computational paradigm that promises significant speedup over classical computing on some problems. Quantum computations are often represented as complex circuits involving quantum “gates”, which are analogous to the logic gates in conventional computers.
However, the difficulty of building quantum computers means that the circuit layouts available in current quantum hardware are comparatively simple. Quantum compilers are programs that map the complex circuitry of quantum computation specifications onto the simpler circuits available today.
Circuit mapping often involves heavy use of the swap gate, which swaps the states of two adjacent quantum bits, or qubits. Through one or more swaps, a qubit state can move through the circuit until it’s adjacent to the next qubit it needs to interact with. But swap gates are costly and error-prone, so the compiler should minimize them.
In a paper we presented at the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT), we propose a novel method that uses automated reasoning to find circuit mappings that minimize the number of swap gates. Satisfiability (SAT) problems are problems that can be stated as expressions of Boolean (binary) variables and logical operations, and the question is whether there is an assignment of values to the variables that satisfies the expressions’ logical constraints.
In our method, a limit on the number of swap gates is one of the constraints that must be satisfied, and a SAT solver tells us whether it can be or not. In a comprehensive evaluation on practical instances over various quantum devices and algorithms, our approach proved 26 times as fast as state-of-the-art solver-based methods, reducing the compilation time from hours to minutes for important quantum applications. Compared to current heuristic algorithms, our method reduces the swap count by 26%, on average.
This is a joint project between Amazon’s Automated-Reasoning Group (ARG) and quantum team (Amazon Braket). I was a student intern when the work was done, so we were eligible for the SAT 2024 Best Student Paper Award, and we finished as runners-up.
Circuit mapping
In the same way that logic gates are the basic building blocks of classical computation, quantum gates are the building blocks of quantum computation. But quantum gating involves manipulating a quantum system in some way — say, changing its magnetic field — so quantum gates, unlike conventional logic gates, are applied at particular points in time. The swap gate is one of the basic quantum gates; others include the Hadamard gate, which puts a qubit into superposition (a mixture of different possible states), and the rotation gate.
We illustrate the problem of quantum circuit mapping with an example. In the figure below, the schematic at left represents the qubit connectivity of (part of) the Rigetti Aspen M-3 quantum computer. Circles are physical qubits, and lines are physical links that allow the application of two-qubit gates.
The figure at right is the circuit diagram of a three-qubit quantum circuit for the famous quantum Fourier transform (QFT) algorithm. The three horizontal lines represent the time schedules of the quantum gates on the three algorithmic qubits. The boxes labeled H indicate one-qubit Hadamard gates, and the boxes labeled R, with connections to solid dots, represent two-qubit controlled rotation gates. The QFT circuit has a two-qubit rotation gate between each two-qubit subset of the three qubits.
Executing the QFT circuit on the Aspen M-3 device requires a quantum compiler to do circuit mapping. Circuit mapping involves two steps: initial qubit placement and qubit routing. During initial qubit placement, the quantum compiler maps each algorithmic qubit in the circuit to a physical qubit on the device, as shown below.
The QFT circuit requires each algorithmic qubit to interact with the other two. However, on the qubit connectivity graph of Aspen M-3, no subgraph forms a three-qubit ring that would allow pairwise qubit interaction. As a result, after initial qubit placement (at left in the figure below), the QFT circuit cannot be directly executed. This type of limitation necessitates the second step in circuit mapping: qubit routing.
Qubit routing is performed by inserting quantum swap gates. After a swap, any gates that, in the computation specification, are targeted to one of the swapped qubits must be re-targeted to its new location. The right-hand figure below denotes swap insertion as two crosses connected by a vertical line. From the example, we can see that swap gates can alter the connectivity requirements of the computation specification to match them with the qubit connectivity of the underlying quantum hardware.
Optimization
Currently, there are two primary approaches to the circuit-mapping problem, solver-based and heuristics-based algorithms. Both approaches have their drawbacks: solver-based algorithms achieve optimal swap count but suffer from long compilation time; heuristic algorithms are fast, but the swap counts are usually suboptimal.
We propose a novel circuit-mapping method based on incremental and parallel solving for Boolean satisfiability (SAT). The figure below presents the framework of our method. We aim to find the minimum number of swap gates that can accommodate the circuit-mapping requirement by iteratively decreasing the swap gate count (S) and checking feasibility with a SAT solver.
Given three inputs — a quantum circuit, a quantum device (QPU), and an initial swap count (S) — we encode the quantum-circuit-mapping problem into a SAT formula in conjunctive normal form (CNF). A SAT solver takes the CNF as input and checks its satisfiability. A satisfiable (SAT) result indicates that there is a valid mapping that uses no more than S swap gates. In this case, we reduce the swap count S and continue the loop to search for a mapping with fewer swap gates. We exit the loop when the solver returns UNSAT, which indicates that we cannot decrease the swap count. Finally, we decode a mapped circuit from the best result we’ve obtained so far.
We developed an efficient implementation to solve the encoded circuit-mapping problem. We use an incremental SAT encoding to iteratively reduce the swap count S and solve the problem without re-encoding the entire problem at every iteration. Hence, the solver can reuse the internal state from the previous iterations to reduce the overall runtime across iterations. We further designed a tailored solver to utilize parallel solving techniques to improve the incremental solving performance.
A comprehensive evaluation on real-world quantum algorithms and devices demonstrates that our method is 26 times as fast as the existing solver-based approach and produces better results. Our method also improved on the heuristic approach on 76% of instances and achieved an average of 26% reduction in swap count.
