A SAT Scalpel for Lattice Surgery: Representation and Synthesis of Subroutines for Surface-Code Fault-Tolerant Quantum Computing

TL;DR

This work formulates lattice-surgery subroutine synthesis (LaS) as a constraint-satisfaction problem and introduces LaSre, a native representation, together with LaSsynth, a SAT-based synthesizer that exhaustively searches the LaS design space. By linking pipe diagrams to correlation surfaces and ZX calculus verification, it enables provably correct and highly optimized LaS designs. Empirically, LaSsynth achieves substantial spacetime-volume reductions across graph-state generation, non-Clifford subroutines (e.g., majority gates), and 15-to-1 $T$-factories, suggesting meaningful reductions in resource requirements for FTQC. The approach holds promise for automated integration into full FTQC compilers, enabling scalable, architecture-aware optimization of critical fault-tolerant building blocks.

Abstract

Quantum error correction is necessary for large-scale quantum computing. A promising quantum error correcting code is the surface code. For this code, fault-tolerant quantum computing (FTQC) can be performed via lattice surgery, i.e., splitting and merging patches of code. Given the frequent use of certain lattice-surgery subroutines (LaS), it becomes crucial to optimize their design in order to minimize the overall spacetime volume of FTQC. In this study, we define the variables to represent LaS and the constraints on these variables. Leveraging this formulation, we develop a synthesizer for LaS, LaSsynth, that encodes a LaS construction problem into a SAT instance, subsequently querying SAT solvers for a solution. Starting from a baseline design, we can gradually invoke the solver with shrinking spacetime volume to derive more compact designs. Due to our foundational formulation and the use of SAT solvers, LaSsynth can exhaustively explore the design space, yielding optimal designs in volume. For example, it achieves 8% and 18% volume reduction respectively over two states-of-the-art human designs for the 15-to-1 T-factory, a bottleneck in FTQC.

Figures (18)

• Figure 1: Fault-tolerant quantum computation based on the surface code. a) The layout of physical qubits. Red faces stand for four-body or two-body $X$ stabilizers; blue faces are $Z$ stabilizers. We shall use color mapping ($X$,$Y$,$Z$) $\mapsto$ (R,G,B) in this paper. b) An example logical operation: merging two separate tiles to a rectangular patch. The stabilizers (faces in a) for the left tile in the beginning are drawn. $d$ QEC rounds are performed after the merge. (Some rounds are omitted.) In the 3D spacetime, the boundaries of code patches (on the qubit plane) sweeping through time produce "pipes".
• Figure 2: Lattice-surgery subroutine (LaS). a) Externals of a LaS implementing a CNOT with four ports and $2\times 2 \times 2$ volume. b) LaS specification including volume, port layout, and functionality (stabilizer) information.
• Figure 3: Overview of contributions (blue numbers). Solid arrows represent the main workflow. Dashes show the verification workflow for existing designs.
• Figure 4: Surface code operations. a) Surface code tile (simplest patch). b-g) Single-patch operations. h) Multiple-patch operation with lattice surgery.
• Figure 5: Logical CNOT in different representations. a) 2D time slices for lattice surgery. The floorplan is in the upper-left corner ($C$: control, $T$: target, $A$: ancilla). 1-3) show the first merge-split. 5-7) show the second merge-split. 0), 4), and 8) are the states between these operations. b) 3D pipe diagram for lattice surgery. We mark the time slices in a) on the time axis. c) CNOT quantum circuit using parity measurements. Slice 1) includes the initialization. Slice 7) includes the $X$ measurement. d) ZX calculus. Junctions of pipes correspond to ZX spiders. The whole pipe diagram maps to the ZX diagram of a CNOT.