pith. machine review for the scientific record. sign in

arxiv: 2604.12560 · v1 · submitted 2026-04-14 · 🪐 quant-ph · cs.ET

Recognition: unknown

Design automation and space-time reduction for surface-code logical operations using a SAT-based EDA kernel compatible with general encodings

Rei Tokami, Wang Liao, Yasunari Suzuki

Pith reviewed 2026-05-10 15:38 UTC · model grok-4.3

classification 🪐 quant-ph cs.ET
keywords surface codelattice surgerylogical CNOTSAT solverfault-tolerant quantum computingdesign automationpatch rotationspace-time cost
0
0 comments X

The pith

KOVAL-Q uses SAT solving to find minimum cycle counts for surface-code CNOTs and patch rotations

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces KOVAL-Q as a satisfiability solver that treats surface-code logical operations as a search problem over flexible patch encodings. It encodes constraints for correct functionality, fault tolerance, and space-time volume to prove the shortest possible schedules for operations like d-cycle CNOTs and 2d-cycle rotations. These shorter schedules are then substituted into standard fault-tolerant algorithms. Under a simplified model the substitution shortens overall application runtime by about 10 percent. The solver is split into three subkernels so it can serve as a module inside larger heuristic optimizers.

Core claim

KOVAL-Q formulates surface-code logical operations as SAT problems that encode functionality, fault tolerance, and space-time costs while supporting general encodings for both target and intermediate states, allowing it to determine the minimum execution time of d-cycle logical CNOTs and 2d-cycle patch rotations and thereby reduce the execution time of widely studied FTQC applications by about 10 percent under a simplified scheduling model.

What carries the argument

The three subkernels that separately encode functionality constraints, fault-tolerance constraints, and space-time cost constraints inside a SAT solver, supporting arbitrary surface-code patch layouts and intermediate states.

If this is right

  • Standard FTQC applications can adopt the shorter CNOT and rotation schedules to finish in fewer total cycles.
  • The optimality proofs hold inside the spatial layouts and encoding families that were searched.
  • The modular subkernels can be dropped into heuristic or hybrid design flows without rewriting the entire optimizer.
  • Advanced layouts such as fast blocks become searchable targets rather than hand-crafted exceptions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same constraint encoding could be reused to compare surface-code performance against other error-correcting codes on identical tasks.
  • Resource estimates for end-to-end quantum algorithms would tighten if these cycle-minimal primitives replaced textbook schedules.
  • Extending the SAT model to include measurement-based or teleportation-based operations might reveal further time savings at the cost of larger search spaces.

Load-bearing premise

The SAT encoding correctly captures how any arrangement of surface-code patches interacts, stays fault tolerant, and incurs the stated space-time cost.

What would settle it

A full circuit-level error simulation of one optimized d-cycle CNOT that shows either a higher logical error rate than the model predicts or a requirement for more than d cycles to complete.

Figures

Figures reproduced from arXiv: 2604.12560 by Rei Tokami, Wang Liao, Yasunari Suzuki.

Figure 1
Figure 1. Figure 1: Surface-code logical qubits with boundaries [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Lattice-surgery-based CNOT gate horizontal face: measurement vertical face: boundary stack at time code distance d d code cycle idling qubits horizontal face: initialization (a) Stabilizer face definition 1 code cycle I J K qubit for merging disassemble 3(J-) 2(J+) 4(K+) 1(I-) 5(K-) 0(I+) 0 8 10 4 1 9 11 5 2 7 6 3 face index edge index (b) Exploration domain and indices [PITH_FULL_IMAGE:figures/full_fig_p… view at source ↗
Figure 3
Figure 3. Figure 3: Definition of stabilizer faces and exploration [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Topological expression of lattice-surgery operations, variables and constraints for LS-SAT [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Topological expression of stabilizer flow, variables, and constraints for Func-SAT formula [PITH_FULL_IMAGE:figures/full_fig_p004_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: FT-SAT explanation (a) reachable faces of one [PITH_FULL_IMAGE:figures/full_fig_p005_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: KOVAL-Q kernel in optimization and verification [PITH_FULL_IMAGE:figures/full_fig_p006_7.png] view at source ↗
Figure 12
Figure 12. Figure 12: Single-qubit patch rotation: (a) a 2-beat operation [PITH_FULL_IMAGE:figures/full_fig_p007_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Lattice surgery operation of 1-beat CNOT using [PITH_FULL_IMAGE:figures/full_fig_p008_13.png] view at source ↗
read the original abstract

Fault-tolerant quantum computers (FTQCs) based on surface codes and lattice surgery have been widely studied, and there is strong demand for a framework that can identify logical operations with low space-time cost, verify their functionality and fault tolerance, and demonstrate their optimality within a given search space, much like electronic design automation (EDA) in classical circuit design. In this paper, we propose KOVAL-Q, an EDA kernel that verifies and optimizes surface-code logical operations by formulating them as a satisfiability (SAT) problem. Compared with existing SAT-based frameworks such as LaSsynth, our method can handle logical qubits with more flexible surface-code encodings, both as target configurations and as intermediate states. This extension enables the optimization of advanced layouts, such as fast blocks, and broadens the search space for logical operations. We demonstrate that KOVAL-Q can determine the minimum execution time of fundamental logical operations in given spatial layouts, such as $d$-cycle logical CNOTs and $2d$-cycle patch rotations. Their use reduces the execution time of widely studied FTQC applications by about 10% under a simplified scheduling model. KOVAL-Q consists of three subkernels corresponding to different types of constraints, which facilitates its integration as a submodule into scalable heuristic frameworks. Thus, our proposal provides an essential framework for optimizing and validating core FTQC subroutines.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper introduces KOVAL-Q, a SAT-based EDA kernel for verifying and optimizing surface-code logical operations under flexible encodings (both targets and intermediate states) that extends beyond prior frameworks such as LaSsynth. It formulates functionality, fault tolerance, and space-time cost as three independent SAT subkernels, demonstrates that the solver finds minimum execution times for d-cycle logical CNOTs and 2d-cycle patch rotations in given layouts, and reports that incorporating these operations reduces the execution time of standard FTQC applications by approximately 10% under a simplified scheduling model.

Significance. If the SAT encoding is shown to be sound for the extended class of layouts and states, the work supplies a modular, parameter-free verification-and-optimization primitive that can be embedded in larger heuristic design flows. The explicit separation into three subkernels and the absence of fitted parameters in the core formulation are clear strengths that facilitate reproducibility and integration.

major comments (2)
  1. [SAT encoding of fault tolerance (methods section describing the three subkernels)] The central quantitative claims (minimum d-cycle CNOT and 2d-cycle rotation times, plus the 10% application-level reduction) rest on the correctness of the fault-tolerance constraint for arbitrary patch layouts and non-standard intermediate states. No cross-validation against known fault-tolerant schedules, explicit enumeration of error sets for the new states, or comparison with manually verified small-d instances is described; if a stabilizer or measurement pattern relevant only to the extended encodings is omitted, the reported minima are not guaranteed to be fault-tolerant.
  2. [Results on application-level speedup] The simplified scheduling model used to translate the obtained logical-operation schedules into the reported 10% application speedup is not specified in sufficient detail (e.g., how idle patches, measurement rounds, and routing are costed). Without an explicit definition or a table comparing baseline versus optimized schedules, the application-level claim cannot be independently assessed.
minor comments (2)
  1. [Notation and figures] Notation for patch boundaries and intermediate stabilizer measurements should be defined once in a dedicated table or figure caption rather than re-introduced inline.
  2. [Introduction and related work] The manuscript would benefit from a short paragraph contrasting the new encoding's variable set with that of LaSsynth to make the extension concrete.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed review. The two major comments highlight important points regarding verification of the fault-tolerance encoding and the transparency of the application-level scheduling model. We address each comment below and will incorporate the requested clarifications and additional material in the revised manuscript.

read point-by-point responses

  1. Referee: [SAT encoding of fault tolerance (methods section describing the three subkernels)] The central quantitative claims (minimum d-cycle CNOT and 2d-cycle rotation times, plus the 10% application-level reduction) rest on the correctness of the fault-tolerance constraint for arbitrary patch layouts and non-standard intermediate states. No cross-validation against known fault-tolerant schedules, explicit enumeration of error sets for the new states, or comparison with manually verified small-d instances is described; if a stabilizer or measurement pattern relevant only to the extended encodings is omitted, the reported minima are not guaranteed to be fault-tolerant.

    Authors: We agree that explicit validation of the generalized fault-tolerance encoding is necessary to support the quantitative claims. The fault-tolerance subkernel encodes the requirement that no weight-1 or weight-2 error on the data or measurement qubits can produce a logical error, using the stabilizer parity-check matrix extended to arbitrary patch boundaries and intermediate merged/split states. To strengthen the manuscript, we will add a dedicated validation subsection that (i) reproduces known minimal d-cycle CNOT schedules from the lattice-surgery literature for standard encodings, (ii) enumerates all weight-1 and weight-2 error syndromes for d=3 fast-block layouts and confirms they are detected by the SAT-derived stabilizers, and (iii) compares the solver output against manually constructed minimal schedules for two small instances. These additions will be placed in the Results section immediately after the description of the three subkernels. revision: yes

  2. Referee: [Results on application-level speedup] The simplified scheduling model used to translate the obtained logical-operation schedules into the reported 10% application speedup is not specified in sufficient detail (e.g., how idle patches, measurement rounds, and routing are costed). Without an explicit definition or a table comparing baseline versus optimized schedules, the application-level claim cannot be independently assessed.

    Authors: We acknowledge that the current description of the scheduling model is too terse. In the revised manuscript we will expand the relevant paragraph in the Results section to define the model precisely: each logical operation is assigned its SAT-derived cycle count; idle patches contribute only their spatial footprint (no extra time cost); each measurement round costs exactly one cycle; and routing between patches is costed as the minimum number of additional cycles required for non-overlapping movement under the surface-code lattice. We will also insert a new table that lists, for each benchmark application, the cycle breakdown of the baseline schedule (standard lattice-surgery CNOTs and rotations) versus the optimized schedule (incorporating the d-cycle CNOTs and 2d-cycle rotations), together with the resulting total runtime and percentage reduction. This will enable independent verification of the reported ~10% improvement under the stated assumptions. revision: yes

Circularity Check

0 steps flagged

No circularity: SAT instance is formulated independently of target minima

full rationale

The paper encodes surface-code operations as a SAT problem whose constraints for functionality, fault tolerance, and space-time cost are stated separately from the claimed minimum execution times. The reported d-cycle CNOT and 2d-cycle rotation minima are direct solver outputs for given layouts; no equation or self-citation reduces these times back to quantities chosen to match the output. The extension beyond LaSsynth encodings is presented as an implementation choice whose soundness is an external verification question, not a definitional loop. The derivation chain therefore remains self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the assumption that standard surface-code lattice surgery rules and fault-tolerance conditions can be faithfully encoded as SAT constraints; no new physical entities or fitted constants are introduced.

axioms (2)
  • domain assumption Surface-code patch movement, merging, and splitting operations preserve logical information and fault tolerance when performed according to lattice-surgery rules.
    Invoked when the SAT constraints are defined for logical CNOTs and patch rotations.
  • domain assumption The simplified scheduling model used to measure the 10% application-level speedup accurately reflects real FTQC resource costs.
    Stated when the authors translate per-operation cycle counts into overall application runtime.

pith-pipeline@v0.9.0 · 5555 in / 1537 out tokens · 56057 ms · 2026-05-10T15:38:15.010336+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

34 extracted references · 22 canonical work pages · 3 internal anchors

  1. [1]

    Scott Aaronson and Daniel Gottesman. 2004. Improved simulation of stabilizer circuits.Physical Review A—Atomic, Molecular, and Optical Physics70, 5 (2004), 052328

    2004

  2. [2]

    Berry, Nathan Wiebe, Jarrod McClean, Alexandru Paler, Austin Fowler, and Hartmut Neven

    Ryan Babbush, Craig Gidney, Dominic W. Berry, Nathan Wiebe, Jarrod McClean, Alexandru Paler, Austin Fowler, and Hartmut Neven. 2018. Encoding Electronic Spectra in Quantum Circuits with Linear T Complexity.Physical Review X8, 4 (Oct. 2018). doi:10.1103/physrevx.8.041015

    work page doi:10.1103/physrevx.8.041015 2018

  3. [3]

    Assessing requirements to scale to practical quantum advantage

    Michael E. Beverland, Prakash Murali, Matthias Troyer, Krysta M. Svore, Torsten Hoefler, Vadym Kliuchnikov, Guang Hao Low, Mathias Soeken, Aarthi Sundaram, and Alexander Vaschillo. 2022. Assessing requirements to scale to practical quantum advantage. doi:10.48550/ARXIV.2211.07629

    work page internal anchor Pith review doi:10.48550/arxiv.2211.07629 2022

  4. [4]

    Héctor Bombín and Miguel Angel Martin-Delgado. 2009. Quantum measurements and gates by code deformation.Journal of Physics A: Mathematical and Theoretical 42, 9 (2009), 095302

    2009

  5. [5]

    S. B. Bravyi and A. Yu. Kitaev. 1998. Quantum codes on a lattice with boundary. doi:10.48550/ARXIV.QUANT-PH/9811052

    work page doi:10.48550/arxiv.quant-ph/9811052 1998

  6. [6]

    Jerry Chow, Oliver Dial, and Jay Gambetta. 2021. IBM Quantum breaks the 100-qubit processor barrier. https://www.ibm.com/quantum/blog/127-qubit- quantum-processor-eagle. Accessed: 2026-04-13

    2021

  7. [7]

    arXiv preprint arXiv:1808.06709 , year=

    Austin G. Fowler and Craig Gidney. 2018. Low overhead quantum computation using lattice surgery. doi:10.48550/ARXIV.1808.06709

    work page doi:10.48550/arxiv.1808.06709 2018

  8. [8]

    Fowler, Matteo Mariantoni, John M

    Austin G. Fowler, Matteo Mariantoni, John M. Martinis, and Andrew N. Cleland

  9. [9]

    Surface codes: Towards practical large-scale quantum computation.Physical Review A86, 3 (Sept. 2012). doi:10.1103/physreva.86.032324

    work page doi:10.1103/physreva.86.032324 2012

  10. [10]

    Craig Gidney. 2017. Factoring with n+2 clean qubits and n-1 dirty qubits. doi:10. 48550/ARXIV.1706.07884

    work page arXiv 2017

  11. [11]

    Google Quantum AI. 2023. Suppressing quantum errors by scaling a surface code logical qubit.Nature614, 7949 (2023), 676–681

    2023

  12. [12]

    Google Quantum AI and Collaborators. 2025. Quantum error correction below the surface code threshold.Nature638, 8052 (2025), 920–926

    2025

  13. [13]

    Kou Hamada, Yasunari Suzuki, and Yuuki Tokunaga. 2024. Efficient and high- performance routing of lattice-surgery paths on three-dimensional lattice. doi:10. 48550/ARXIV.2401.15829

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  14. [14]

    Language Model Cascades: Token-Level Uncertainty and Beyond

    Tianyi Hao, Joseph Sullivan, Sivaprasad Omanakuttan, Michael A. Perlin, and Ruslan Shaydulin. 2025. Compilation Pipeline for Predicting Algorithmic Break- Even in an Early-Fault-Tolerant Surface Code Architecture. doi:10.48550/ARXIV. 2511.20947

    work page internal anchor Pith review doi:10.48550/arxiv 2025

  15. [15]

    Dominic Horsman, Austin G Fowler, Simon Devitt, and Rodney Van Meter. 2012. Surface code quantum computing by lattice surgery.New Journal of Physics14, 12 (2012), 123011

    2012

  16. [16]

    Shuwen Kan, Zefan Du, Chenxu Liu, Meng Wang, Yufei Ding, Ang Li, Ying Mao, and Samuel Stein. 2025. SPARO: Surface-code Pauli-based Architectural Resource Optimization for Fault-tolerant Quantum Computing. arXiv:2504.21854 [quant- ph] https://arxiv.org/abs/2504.21854

    work page arXiv 2025

  17. [17]

    A Yu Kitaev. 1997. Quantum computations: algorithms and error correction. Russian Mathematical Surveys52, 6 (1997), 1191

    1997

  18. [18]

    Takumi Kobori, Yasunari Suzuki, Yosuke Ueno, Teruo Tanimoto, Synge Todo, and Yuuki Tokunaga. 2025. LSQCA: Resource-Efficient Load/Store Architecture for Limited-Scale Fault-Tolerant Quantum Computing. In2025 IEEE International Symposium on High Performance Computer Architecture (HPCA). IEEE, 304–320. doi:10.1109/hpca61900.2025.00033

    work page doi:10.1109/hpca61900.2025.00033 2025

  19. [19]

    Sebastian Krinner, Nathan Lacroix, Ants Remm, Agustin Di Paolo, Elie Genois, Catherine Leroux, Christoph Hellings, Stefania Lazar, Francois Swiadek, Johannes Herrmann, et al. 2022. Realizing repeated quantum error correction in a distance- three surface code.Nature605, 7911 (2022), 669–674

    2022

  20. [20]

    Nathan Lacroix, Alexandre Bourassa, Francisco JH Heras, Lei M Zhang, Jo- hannes Bausch, Andrew W Senior, Thomas Edlich, Noah Shutty, Volodymyr Sivak, Andreas Bengtsson, et al. 2025. Scaling and logic in the colour code on a superconducting quantum processor.Nature645, 8081 (May 2025), 614–619. doi:10.1038/s41586-025-09061-4

    work page doi:10.1038/s41586-025-09061-4 2025

  21. [21]

    Landahl and Jonas T

    Andrew J. Landahl, Jonas T. Anderson, and Patrick R. Rice. 2011. Fault-tolerant quantum computing with color codes. doi:10.48550/ARXIV.1108.5738

    work page doi:10.48550/arxiv.1108.5738 2011

  22. [22]

    Daniel Litinski. 2019. A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery.Quantum3 (March 2019), 128. doi:10.22331/q-2019-03-05- 128

    work page doi:10.22331/q-2019-03-05- 2019

  23. [23]

    Daniel Litinski. 2019. Magic state distillation: Not as costly as you think.Quantum 3 (2019), 205

    2019

  24. [24]

    Abtin Molavi, Amanda Xu, Swamit Tannu, and Aws Albarghouthi. 2025. Dependency-Aware Compilation for Surface Code Quantum Architectures. Proc. ACM Program. Lang.9, OOPSLA1, Article 82 (April 2025), 28 pages. doi:10.1145/3720416

    work page doi:10.1145/3720416 2025

  25. [25]

    Lukin, and Hengyun Zhou

    Christopher Pattison, Gefen Baranes, Juan Pablo Bonilla Ataides, Mikhail D. Lukin, and Hengyun Zhou. 2025. Constant-Rate Entanglement Distillation for Fast Quantum Interconnects. InProceedings of the 52nd Annual International Symposium on Computer Architecture (SIGARCH ’25). ACM, 257–270. doi:10.1145/ 3695053.3731069

    work page arXiv 2025

  26. [26]

    Quration Developers. 2026. Quration: Quantum Resource Estimation Toolchain. https://github.com/quration/quration. Accessed: 2026-04-13

    2026

  27. [27]

    Riesebos, X

    L. Riesebos, X. Fu, S. Varsamopoulos, C. G. Almudever, and K. Bertels. 2017. Pauli Frames for Quantum Computer Architectures. InProceedings of the 54th Annual Design Automation Conference 2017 (DAC ’17). ACM, 1–6. doi:10.1145/3061639. 3062300

    work page doi:10.1145/3061639 2017

  28. [28]

    and Selinger, Peter , keywords =

    Neil J. Ross and Peter Selinger. 2014. Optimal ancilla-free Clifford+T approxima- tion of z-rotations. (2014). doi:10.48550/ARXIV.1403.2975

    work page doi:10.48550/arxiv.1403.2975 2014

  29. [29]

    Allyson Silva, Xiangyi Zhang, Zak Webb, Mia Kramer, Chan-Woo Yang, Xiao Liu, Jessica Lemieux, Ka-Wai Chen, Artur Scherer, and Pooya Ronagh. 2024. Multi- qubit Lattice Surgery Scheduling.LIPIcs, Volume 310, TQC 2024310, 1:1–1:22. doi:10.4230/LIPICS.TQC.2024.1

    work page doi:10.4230/lipics.tqc.2024.1 2024

  30. [30]

    Daniel Bochen Tan, Murphy Yuezhen Niu, and Craig Gidney. 2024. A SAT Scalpel for Lattice Surgery: Representation and Synthesis of Subroutines for Surface-Code Fault-Tolerant Quantum Computing . In2024 ACM/IEEE 51st Annual International Symposium on Computer Architecture (ISCA). IEEE Computer Society, Los Alamitos, CA, USA, 325–339. doi:10.1109/ISCA59077.2...

    work page doi:10.1109/isca59077.2024.00032 2024

  31. [31]

    Riki Toshio, Shota Kanasugi, Jun Fujisaki, Hirotaka Oshima, Shintaro Sato, and Keisuke Fujii. 2026. STAR-Magic Mutation: Even More Efficient Analog Rotation Gates for Early Fault-Tolerant Quantum Computer. doi:10.48550/ARXIV.2603. 22891

    work page doi:10.48550/arxiv.2603 2026

  32. [32]

    Chong, and Jakub Szefer

    Theodoros Trochatos, Christopher Kang, Andrew Wang, Frederic T. Chong, and Jakub Szefer. 2025. Trace-Based Reconstruction of Quantum Circuit Dataflow in Surface Codes. arXiv:2508.14533 [quant-ph] https://arxiv.org/abs/2508.14533

    work page arXiv 2025

  33. [33]

    George Watkins, Hoang Minh Nguyen, Keelan Watkins, Steven Pearce, Hoi-Kwan Lau, and Alexandru Paler. 2024. A High Performance Compiler for Very Large Scale Surface Code Computations.Quantum8 (May 2024), 1354. doi:10.22331/q- 2024-05-22-1354

    work page doi:10.22331/q- 2024

  34. [34]

    Nobuyuki Yoshioka, Tsuyoshi Okubo, Yasunari Suzuki, Yuki Koizumi, and Wataru Mizukami. 2024. Hunting for quantum-classical crossover in condensed matter problems.npj Quantum Information10, 1 (2024), 45

    2024