Pith. sign in

REVIEW 3 major objections 4 minor 56 references

Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper formalizes dirty-qubit borrowing, proves the scheduling problem NP-hard, and presents Bona, a depth-aware heuristic that reuses nearly 99% of dirty ancillas on benchmark circuits while keeping depth overhead controlled.

desk verdict Good practical scheduler with an elegant graph model, but the NP-hardness proof has a gap that should be fixed before the theory headline is fully trusted. read the letter →

arxiv 2608.08765 v1 pith:QFUOUYHR submitted 2026-08-09 cs.PL quant-ph

Xiaoquan Xu , Chenke Liu , Boning Meng , Zihao Shen , Li Zhou This is my paper · ORCID
classification cs.PLquant-ph MSC 68Q1781P68
keywords dirtyancillaqubitborrowingcircuitwidthoptimizationquantumdepthNP-completenessedgesplicingEndpointDAGscheduling
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Dirty ancillas are qubits borrowed from temporarily idle wires, used without knowing their initial state, and then restored, letting a compiler shrink circuit width (the number of qubits the computation needs at once). This paper tries to establish that dirty-ancilla management can be automated: it defines a formal transition system for borrowing, proves the scheduling optimization NP-hard, and presents Bona, a depth-aware heuristic scheduler. On benchmark circuits Bona eliminates 99–100% of dirty ancillas in parallel quantum walk and cuts Shor's dirty ancillas from 192–6400 down to 3–20, with depth overhead at most 20%. In parallel circuits the paper finds a scheduling advantage: after optimization, dirty-ancilla circuits match clean-ancilla width while ending up significantly shallower. If right, this makes dirty ancillas a compiler-managed resource rather than a hand-crafted trick.

What carries the argument

The load-bearing object is the Endpoint DAG, a directed acyclic graph whose edges trace each qubit's temporal flow through the circuit, with dirty ancillas marked as distinguished qubits. Borrowing is reformulated as edge-splicing: to borrow a dirty ancilla $d$ into an idle edge $(u,v)$, cut $(u,v)$ and insert $d$'s operation path between $u$ and $v$; the step is valid exactly when $\mathrm{fst}(d)$ is not reachable from $u$ and $v$ is not reachable from $\mathrm{lst}(d)$, which prevents cycles. This characterization carries both halves of the paper: it makes the NP-hardness reduction tractable, and it gives Bona its depth-aware selection rule, a look-ahead cost $c_{\Delta d}$ estimating how much a splice stretches the critical path, with zero-cost soft splices handled through an interval pool and costly hard splices through a graph-wide scan.

What would settle it

Take a small unsatisfiable 3-SAT formula, build the Endpoint DAG exactly as in the reduction, and enumerate all valid edge-splicing sequences; if any sequence maps every dirty ancilla while keeping the graph acyclic, the reduction's claim that unsatisfiability forces a failure is wrong and NP-hardness collapses. A weaker probe: on a satisfiable instance, find a complete borrowing assignment in which a dirty path is spliced into a working path not of the prescribed lower-indexed form, which would contradict the order-dependence lemma.

Watch

Extended reading notes

Core claim

The central claim is that deciding whether every dirty ancilla can be mapped away—the Complete-Borrowing problem—is NP-complete, so exact optimal scheduling of width and depth is intractable in general, yet the same graph formulation supports a near-optimal practical scheduler. The paper proves hardness by reducing 3-SAT through a new graph problem, DAG-in-UDG, to borrowing on the Endpoint DAG, and shows depth-aware variants of the optimization are NP-hard as well. For practice, Bona greedily splices dirty ancillas into idle edges, preferring zero-depth soft borrows found through an interval pool and reserving graph-wide hard searches for the rest, and the paper proves each splice satisfies the unreachable condition, so the output circuit is semantically equivalent to the input. Empirically, Bona reduces dirty-ancilla usage by nearly 99% on average, matches manual optimization in width on three of four component benchmarks, and on parallel quantum walk attains clean-ancilla width with substantially smaller depth.

Load-bearing premise

The NP-hardness proof depends on a fixed splice order: it assumes a dirty path can only enter one specific position because all earlier positions are already filled, and if valid borrowings can occur in a different order, the constructed hard instances might have unintended complete solutions and the hardness collapse.

Editorial extensions

If this is right

  • Because Complete-Borrowing is NP-complete, exact optimal dirty-ancilla scheduling is out of reach for large circuits, and heuristic schedulers such as Bona are the practical route.
  • A compiler can run a clean-ancilla optimizer first and then Bona, since dirty borrowing fills idle gaps that clean recycling leaves behind; this Clean-then-Dirty order reproduces manual optimization on most tested components.
  • On parallel quantum walk and randomly composed parallel circuits, dirty-ancilla circuits optimized with Bona reach essentially the same width as clean-ancilla circuits but end up shallower, which is direct evidence that dirty ancillas are not merely a fallback.
  • Every splice Bona performs obeys the unreachable condition, so its output is guaranteed to be a valid circuit semantically equivalent to the input.
  • If topological reordering is frozen, the minimal width is computable in linear time by a structural recursion, isolating dynamic reordering as the source of hardness.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Given the NP-hardness result, adding hardware-level constraints such as routing or mid-circuit reset can only make scheduling harder, so physical-level dirty-ancilla managers will likely also need heuristics of Bona's kind.
  • Bona's look-ahead cost approximates the true depth change rather than measuring it; comparing it against brute-force optimal schedules on small circuits could measure the approximation gap and guide a better cost function.
  • The Clean-then-Dirty order encodes a general allocation principle—serve the most constrained requests first—that could carry over to other flexible compilation resources, such as reusable mid-circuit measurement slots.
  • The measured crossover between dirty and clean schemes at a certain parallelism level is a testable prediction: on hardware with mid-circuit measurement and reset, dirty borrowing should beat clean recycling in post-optimization depth once parallelism exceeds that threshold.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper formalizes dirty-qubit borrowing in quantum circuits via a small imperative language with explicitly scoped borrow statements and a set of semantics-preserving transitions. It introduces the Endpoint DAG abstraction, proves a step-correspondence theorem between edge-splicing in the DAG and circuit-level borrowing, and claims NP-completeness of the Complete-Borrowing problem through a reduction from DAG-in-UDG. The authors then present Bona, a depth-aware heuristic scheduler, and evaluate it on parallel quantum walk, Shor's algorithm, component-level circuits, and randomly composed RevLib circuits, reporting reductions of roughly 99% in dirty-ancilla usage, moderate depth overheads, and a depth advantage for dirty-ancilla implementations in parallel circuits.

Significance. The Endpoint DAG model and the step-correspondence theorem are a clean conceptual contribution, and the paper is the first to provide an automated scheduler specifically for dirty-ancilla borrowing. The evaluation is broad, includes realistic algorithm instances, and the data-availability statement makes the implementation reproducible, which is a notable strength. The claimed NP-hardness result is central to the paper's theoretical contribution, and the current proof has a load-bearing gap; until that gap is repaired, the hardness results are conditional. If the proof can be completed and the scheduler results are reproducible, the paper would be a solid contribution to quantum circuit compilation.

major comments (3)
  1. [Appendix C, proof of Theorem 5.5] The central claim that a dirty path e[i,m]x can only splice into a working path e[0,i-1]y is not established. The induction step assumes that all paths e[0,j-1]y with 1 <= j <= i-1 "have been spliced", but Complete-Borrowing permits arbitrary splicing order and the unreachable condition of Definition 4.3 does not enforce the index ordering. In the construction itself, a working path e[0,j-1]y with j < i and a dirty path e[i,m]x satisfy the two unreachable tests whenever y is not reachable to x: e_i cannot reach e_{j-1} because all e-edges go forward, and the constructed paths contain no edges from the original vertices back to the e-chain. Thus the crossing splice is locally legal under the paper's own rules. To make the reduction sound, the proof needs an additional argument, for example a rank or counting argument showing that every complete borrowing sequence must splice in nondecreasing index order, and no such argument appears. Without it, the extraction of a UDG realization from the final DAG T' is not well-defined, and Theorem 5.5 is unproven.
  2. [Section 5.2, Corollary 5.6 and the Complexity Landscape] The NP-hardness of Complete-Borrowing is the only route given for Corollary 5.6 and for the width-then-depth and depth-then-width statements. Since the proof of Theorem 5.5 is incomplete (see previous comment), these hardness claims are currently unsupported. In addition, the depth-then-width reduction is only sketched: appending an "extremely long" dummy working qubit that shares gates with every dirty ancilla is asserted to lock the optimal depth, but no argument is given that the construction preserves the width-optimization instance or that the appended gates do not create new borrowing opportunities. The authors should provide a complete reduction or explicitly state these as conjectures.
  3. [Section 7.2.1, Table 1] The abstract's phrase "controlled depth overhead" is stronger than what Table 1 shows for the main PQW results. For the max-ancilla versions, Recycle+Bona increases depth by 101%–330%, while the much smaller overheads of 1%–18% are achieved only after manual preprocessing (the Manual+Bona columns). The claim is defensible if "controlled" is interpreted relative to the large width reduction, but the current wording invites a stronger reading. Please either report the average with the manual-preprocessing qualification stated clearly or adjust the wording in the abstract and introduction.
minor comments (4)
  1. [Section 2.1, Definition of reachability] The paper does not state whether paths of length zero are allowed in the definition of reachability. The unreachable condition in Definition 4.3 and Lemma B.1 rely on this distinction when fst(d) equals u or v equals lst(d), since a self-loop would then be created. Please clarify that reachability is reflexive in these arguments.
  2. [Appendix C, proof of Lemma 5.4] There are typos: "grantee" should be "guarantee", and "loop" should be "cycle". The wording in the last paragraph, "Then, for every literal y_j in c_j, y_j x_false c c_j forms a path", would be clearer if the path were written as y_j -> x_false -> c -> c_j -> y_j.
  3. [Throughout] The name "Decross" appears in Table 1 while the reference is "DeCross et al."; please use a consistent spelling. Also, the notation "TrivD" and "Manual+TrivD" is used without an explicit definition in the experimental setup; a one-sentence description of the TrivD baseline would improve readability.
  4. [Appendix D.2] The implementation appendix describes a restriction that boundary nodes of dirty ancillas are not exposed during the initial sweep, so that dirty-dirty recycling is postponed. This behavior is not present in Algorithm 1 in Section 6.2, which pools all edges. Please state explicitly that Algorithm 1 is a graph-theoretic abstraction and that the OpGrid implementation adds this policy, so the reader can match the algorithm description to the implementation.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the Endpoint DAG model and NP-hardness chain are independent of the paper's own conclusions; the Appendix C proof gap is a correctness risk, not a circularity.

full rationale

The paper's central claims are the NP-hardness of dirty-qubit borrowing and the effectiveness of the Bona scheduler. Neither reduces by construction to its inputs. The Endpoint DAG model is justified by Lemma 4.1 and Theorem 4.4, whose proofs construct the correspondence between edge-splicing and circuit-level borrowing rather than assuming it. Bona is a deterministic heuristic evaluated against external benchmarks (PQW, Shor, RevLib, and published component circuits); no parameter is fitted to the reported width or depth numbers, and the claimed 99% dirty-ancilla reduction is an experimental measurement, not a restatement of an input. The NP-hardness proof reduces from 3-SAT through DAG-in-UDG to Complete-Borrowing, which is an independent chain. The converse direction of Theorem 5.5 in Appendix C relies on an asserted induction that dirty paths e[i,m]x can only splice into e[0,i-1]y; the manuscript does not fully justify this order-dependence, and a skeptical reading can construct locally legal splice orders that violate the claimed invariant. This is a possible proof gap and a correctness risk, but it is not circularity: the invariant is not assumed as an input, and its failure would make the reduction unsound rather than tautological. The only overlapping-author citation, [41], is used to note that equivalent formulations of dirty-ancilla safety have been discussed, and it is not load-bearing for any derivation in the paper. Accordingly, the appropriate finding is no significant circularity, score 0.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The formal results rest on the standard safety characterization of dirty ancillas from prior work (Equation 1), the definitional validity conditions of the Endpoint DAG, and the standard complexity-theoretic assumption that 3-SAT is NP-complete. Bona has no fitted parameters; its heuristic is deterministic. No new physical entities are introduced.

assumptions (5)
  • domain assumption A dirty ancilla is used safely iff U = I_a ⊗ V for some unitary V (Equation 1, Section 2.2).
    Adopted from Su et al. [40,41]; the entire formal model of dirty-qubit borrowing depends on this characterization of safety.
  • domain assumption Two subcircuits acting on disjoint qubits may be swapped without changing semantics (Swap rule, Section 3.2).
    Standard for quantum circuits over disjoint qubits; used pervasively in the Endpoint DAG quotient.
  • domain assumption Input circuits are safe, meaning every borrow[.] statement satisfies Equation (1); unsafe circuits evaluate to ⊥ and are excluded.
    This is the input condition for Theorem 6.1; Bona does not verify safety itself.
  • domain assumption The Endpoint DAG validity conditions (acyclic, balanced, I/O consistency) exactly characterize circuits (Lemma 4.1).
    Proved in Appendix B.1; the proof relies on standard facts about DAGs and topological orderings.
  • standard math 3-SAT is NP-complete and reductions are polynomial-time (Section 5).
    Background for the claimed NP-hardness results.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits." pith.science (2026). https://pith.science/paper/QFUOUYHR

@misc{pith2026260808765,
  author       = {Pith},
  title        = {Pith review of: Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QFUOUYHR}},
  note         = {Machine review of arXiv:2608.08765}
}
read the original abstract

The management of ancilla qubits has become a critical technique for reducing quantum circuit width. Dirty ancillas, which may be borrowed from any temporarily idle qubit regardless of their initial states, offer substantial flexibility for width optimization, but their use has so far required manual and error-prone handling. We formalize the dirty-qubit borrowing problem and establish a fundamental computational limit by proving its NP-hardness. To support practical optimization, we present \bona, the first scheduler for dirty-qubit borrowing, built on a novel depth-aware heuristic algorithm. We evaluate \bona~ across a variety of benchmarks, including practical quantum circuits and randomly arranged compositions of real circuit modules, and find that it reduces nearly 99\% of dirty ancillas on average with controlled depth overhead. In particular, for parallel quantum walk---an essential component of parallel Hamiltonian simulation---\bona~ matches the circuit width achieved by the clean-qubit schemes of \citeauthor{jiang2024recycling}~(\citeyear{jiang2024recycling}) and \citeauthor{quantinuum}~(\citeyear{quantinuum}), but attains significantly smaller circuit depth, providing concrete evidence that dirty ancillas offer unique optimization advantages in circuits with certain parallelism.

Figures

Figures reproduced from arXiv: 2608.08765 by the authors.

Figure 1
Figure 1. The transformation from left to right illustrates how an idle middle interval of the top wire can be [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. A quantum circuit (left) with input qubits [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Left: Implementations of C 3NOT using C 2NOT gates and one ancilla. The red dirty-ancilla circuit is fully semantically equivalent to the black target circuit, whereas the blue clean-ancilla circuit is equivalent only when the ancilla is initialized to |0⟩. Right: Implementation of two parallel C 3NOT with recycling, with the clean ancilla marked by an orange line. directs from a predecessor 𝑢 to a successor 𝑣. For … view at source ↗
Figures from the paper (9 more)
Figure 4
Figure 4. Figure 4: A circuit-level illustration of the transition sequence from left to right. Each labeled box represents [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Interleaving topology and borrowing. Borrowing [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: The Endpoint DAG Model as a canonical abstraction. The left panel shows the corresponding formal [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: Borrowing as edge-splicing. In the DAG, substituting [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]
Figure 8
Figure 8. Figure 8: Schematic diagram of the reduction from 3-SAT to [PITH_FULL_IMAGE:figures/full_fig_p014_8.png]
Figure 9
Figure 9. Figure 9: Different depth effects of two feasible borrowing choices. (Left) The initial circuit contains a dirty [PITH_FULL_IMAGE:figures/full_fig_p016_9.png]
Figure 10
Figure 10. Figure 10: Visualizing the components of the depth-aware look-ahead cost [PITH_FULL_IMAGE:figures/full_fig_p016_10.png]
Figure 11
Figure 11. Figure 11: Borrowing schedules for the circuit in Figure [PITH_FULL_IMAGE:figures/full_fig_p018_11.png]
Figure 12
Figure 12. Figure 12: From left to right, the plots show circuit depth, width, and optimization time as parallelism increases [PITH_FULL_IMAGE:figures/full_fig_p024_12.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

56 extracted references · 18 canonical work pages

  1. [1]

    Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, and Wei-Lun Tsai. 2025. Verifying Quantum Circuits with Level-Synchronized Tree Automata.Proc. ACM Program. Lang.9, POPL, Article 32 (Jan. 2025), 31 pages. doi:10.1145/3704868

    doi:10.1145/3704868 2025

  2. [2]

    Chow, Antonio D

    Gadi Aleksandrowicz, Thomas Alexander, Panagiotis Barkoutsos, Luciano Bello, Yael Ben-Haim, David Bucher, Francisco Jose Cabrera-Hernández, Jorge Carballo-Franquis, Adrian Chen, Chun-Fu Chen, Jerry M. Chow, Antonio D. Córcoles-Gonzales, Abigail J. Cross, Andrew Cross, Juan Cruz-Benito, Chris Culver, Salvador De La Puente González, Enrique De La Torre, Del...

    2019

  3. [3]

    Baker, Casey Duckering, Alexander Hoover, and Frederic T

    Jonathan M. Baker, Casey Duckering, Alexander Hoover, and Frederic T. Chong. 2019. Decomposing Quantum Generalized Toffoli with an Arbitrary Number of Ancilla. arXiv:1904.01671 [quant-ph] https://arxiv.org/abs/1904.01671

    arXiv 2019

  4. [4]

    Bennett, Richard Cleve, David P

    Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. 1995. Elementary gates for quantum computation.Phys. Rev. A52 (Nov 1995), 3457–3467. Issue 5. doi:10.1103/PhysRevA.52.3457

    doi:10.1103/physreva.52.3457 1995

  5. [5]

    Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. 2020. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. InProceedings of the 41st ACM SIGPLAN Conference on Programming Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits 27 Language Design and Implementation(London, UK)(PLDI 2020)...

    arXiv 2020

  6. [6]

    Sebastian Brandhofer, Ilia Polian, and Kevin Krsulich. 2023. Optimal Qubit Reuse for Near-Term Quantum Computers. In2023 IEEE International Conference on Quantum Computing and Engineering (QCE), Vol. 01. 859–869. doi:10.1109/ QCE57702.2023.00100

    arXiv 2023

  7. [7]

    Christophe Chareton, Sébastien Bardin, Dong Ho Lee, Benoît Valiron, Renaud Vilmart, and Zhaowei Xu. 2023. Formal Methods for Quantum Algorithms. InHandbook of Formal Analysis and Verification in Cryptography. CRC Press, 319–422. https://cea.hal.science/cea-04479879

    work page 2023

  8. [8]

    Yu-Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. 2023. An automata-based framework for verification and bug hunting in quantum circuits.Proceedings of the ACM on Programming Languages7, PLDI (2023), 1218–1243

    work page 2023

Show all 56 references
  1. [9]

    Matthew DeCross, Eli Chertkov, Megan Kohagen, and Michael Foss-Feig. 2023. Qubit-Reuse Compilation with Mid-Circuit Measurement and Reset.Phys. Rev. X13 (Dec 2023), 041057. Issue 4. doi:10.1103/PhysRevX.13.041057

    2023 doi

  2. [10]

    Yongshan Ding, Xin-Chuan Wu, Adam Holmes, Ash Wiseth, Diana Franklin, Margaret Martonosi, and Frederic T. Chong

  3. [11]

    Kun Fang, Munan Zhang, Ruqi Shi, and Yinan Li. 2023. Dynamic quantum circuit compilation. arXiv:2310.11021 [quant- ph] https://arxiv.org/abs/2310.11021

    2023 arXiv

  4. [12]

    Craig Gidney. 2015. Constructing Large Controlled Nots. https://algassert.com/circuits/2015/06/05/Constructing- Large-Controlled-Nots.html. Accessed: 2025-09-05

    2015

  5. [13]

    Craig Gidney. 2018. Factoring with n+2 clean qubits and n-1 dirty qubits. arXiv:1706.07884 [quant-ph] https: //arxiv.org/abs/1706.07884

    2018 arXiv

  6. [14]

    Lov K. Grover. 1997. Quantum Mechanics Helps in Searching for a Needle in a Haystack.Phys. Rev. Lett.79 (Jul 1997), 325–328. Issue 2. doi:10.1103/PhysRevLett.79.325

    1997 doi

  7. [15]

    Jinyoung Ha, Jonghyun Lee, and Jun Heo. 2024. Resource analysis and modifications of quantum computing with noisy qubits for elliptic curve discrete logarithms.Scientific Reports14, 1 (16 Feb 2024), 3927. doi:10.1038/s41598-024-54434-w

    2024 doi

  8. [16]

    Thomas Häner, Martin Roetteler, and Krysta M. Svore. 2017. Factoring using 2n + 2 qubits with Toffoli based modular multiplication.Quantum Info. Comput.17, 7–8 (June 2017), 673–684

    2017

  9. [17]

    Kengo Hirata and Chris Heunen. 2025. Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime. Proc. ACM Program. Lang.9, POPL, Article 6 (Jan. 2025), 28 pages. doi:10.1145/3704842

    2025 doi

  10. [18]

    Bishop, John Lapeyre, Ali Javadi-Abhari, and Eddy Z

    Fei Hua, Yuwei Jin, Yanhao Chen, Suhas Vittal, Kevin Krsulich, Lev S. Bishop, John Lapeyre, Ali Javadi-Abhari, and Eddy Z. Zhang. 2023. CaQR: A Compiler-Assisted Approach for Qubit Reuse through Dynamic Circuit. InProceedings of the 28th ACM International Conference on Archite...

    2023

  11. [19]

    Zhenyu Huang, Fuxin Zhang, and Dongdai Lin. 2025. Constructing Quantum Implementations with the Minimal T-depth or Minimal Width and Their Applications. InAdvances in Cryptology – EUROCRYPT 2025, Serge Fehr and Pierre-Alain Fouque (Eds.). Springer Nature Switzerland, Cham, 155–185

    2025

  12. [20]

    2019.Sorted List — Sorted Containers 2.4.0 documentation

    Grant Jenks. 2019.Sorted List — Sorted Containers 2.4.0 documentation. https://grantjenks.com/docs/sortedcontainers/ sortedlist.html Licensed under Apache License 2.0

    2019

  13. [21]

    Hanru Jiang. 2024. Qubit Recycling Revisited.Proc. ACM Program. Lang.8, PLDI, Article 198 (June 2024), 24 pages. doi:10.1145/3656428

    2024 doi

  14. [22]

    A. B. Kahn. 1962. Topological sorting of large networks.Commun. ACM5, 11 (Nov. 1962), 558–562. doi:10.1145/ 368996.369025

    1962

  15. [23]

    Tanuj Khattar and Craig Gidney. 2025. Rise of conditionally clean ancillae for efficient quantum circuit constructions. Quantum9 (May 2025), 1752. doi:10.22331/q-2025-05-21-1752

    2025 doi

  16. [24]

    Hyungseok Kim, Enhyeok Jang, Seungwoo Choi, Youngmin Kim, and Won Woo Ro. 2025. QR-Map: A Map-Based Approach to Quantum Circuit Abstraction for Qubit Reuse Optimization. InProceedings of the 52nd Annual International Symposium on Computer Architecture (ISCA ’25). Association f...

    2025

  17. [25]

    Marco Lewis, Sadegh Soudjani, and Paolo Zuliani. 2023. Formal Verification of Quantum Programs: Theory, Tools, and Challenges. 5, 1, Article 1 (dec 2023), 35 pages. doi:10.1145/3624483

    2023 doi

  18. [26]

    Jiqi Li, Jingyi Mei, Wang Fang, and Ji Guan. 2026. Formal Verification of Quantum Ancilla Safety. InComputer Aided Verification (Lecture Notes in Computer Science). Springer. To appear

    2026

  19. [27]

    Guang Hao Low, Vadym Kliuchnikov, and Luke Schaeffer. 2024. Trading T gates for dirty qubits in state preparation and unitary synthesis.Quantum8 (June 2024), 1375. doi:10.22331/q-2024-06-17-1375 28 Xiaoquan Xu, Chenke Liu, Boning Meng, Zihao Shen, and Li Zhou

    2024 doi

  20. [28]

    Junhong Nie, Wei Zi, and Xiaoming Sun. 2024. Quantum circuit for multi-qubit Toffoli gate with optimal resource. arXiv:2402.05053 [quant-ph] https://arxiv.org/abs/2402.05053

    2024 arXiv

  21. [29]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2011.Quantum Computation and Quantum Information: 10th Anniversary Edition(10th ed.). Cambridge University Press, USA

    2011

  22. [30]

    Siyuan Niu, Akel Hashim, Costin Iancu, Wibe Albert De Jong, and Ed Younis. 2024. Effective Quantum Resource Optimization via Circuit Resizing in BQSKit. InProceedings of the 61st ACM/IEEE Design Automation Conference(San Francisco, CA, USA)(DAC ’24). Association for Computing ...

    2024

  23. [31]

    Alexandru Paler, Robert Wille, and Simon J. Devitt. 2016. Wire recycling for quantum circuit optimization.Phys. Rev. A94 (Oct 2016), 042337. Issue 4. doi:10.1103/PhysRevA.94.042337

    2016 doi

  24. [32]

    Anouk Paradis, Benjamin Bichsel, Samuel Steffen, and Martin Vechev. 2021. Unqomp: synthesizing uncomputation in Quantum circuits(PLDI 2021). Association for Computing Machinery, New York, NY, USA, 222–236. doi:10.1145/ 3453483.3454040

    2021

  25. [33]

    Anouk Paradis, Benjamin Bichsel, and Martin Vechev. 2024. Reqomp: Space-constrained Uncomputation for Quantum Circuits.Quantum8 (Feb. 2024), 1258. doi:10.22331/q-2024-02-19-1258

    2024 doi

  26. [34]

    John Preskill. 2025. Beyond NISQ: The Megaquop Machine.ACM Transactions on Quantum Computing6, 3, Article 18 (April 2025), 7 pages. doi:10.1145/3723153

    2025 doi

  27. [35]

    2025.Built-in Types

    Python Software Foundation. 2025.Built-in Types. https://docs.python.org/3/library/stdtypes.html#set©2001-2025 Python Software Foundation. Last updated on Mar 17, 2026

    2025

  28. [36]

    2025.Ancilla-Free Quantum Adder with Sublinear Depth

    Maxime Remaud and Vivien Vandaele. 2025.Ancilla-Free Quantum Adder with Sublinear Depth. Springer Nature Switzerland, 137–154. doi:10.1007/978-3-031-97063-4_11

    2025 doi

  29. [37]

    Movahhed Sadeghi, Soheil Khadirsharbiyani, and Mahmut Taylan Kandemir. 2022. Quantum Circuit Resizing. arXiv:2301.00720 [cs.ET] https://arxiv.org/abs/2301.00720

    2022 arXiv

  30. [38]

    2004.Timing

    Sachin Sapatnekar. 2004.Timing. Springer

    2004

  31. [39]

    Peter W. Shor. 1997. Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer.SIAM J. Comput.26, 5 (Oct. 1997), 1484–1509. doi:10.1137/s0097539795293172

    1997 doi

  32. [40]

    Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying. 2024. BI-based Reasoning about Quantum Programs with Heap Manipulations. arXiv:2409.10153 [quant-ph] https://arxiv.org/abs/2409.10153

    2024 arXiv

  33. [41]

    Bonan Su, Li Zhou, Yuan Feng, and Mingsheng Ying. 2026. Borrowing Dirty Qubits in Quantum Programs. InProceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2(USA)(ASPLOS ’26). Association for Compu...

    2026

  34. [42]

    Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. 2018. Q#: Enabling Scalable Quantum Computing and Devel- opment with a High-level DSL(RWDSL2018). Association fo...

    2018

  35. [43]

    Haotian Tang, Fei Ding, Xueyun Cheng, Shuxian Zhao, and Zhijin Guan. 2025. Width Optimization of Quantum Circuit Based on Reuse-Aimed Quantum Circuit Transformation.Quantum Information & Computation25, 3 (2025), 216–231. doi:10.2478/qic-2025-0011

    2025 doi

  36. [44]

    Hristo Venev, Timon Gehr, Dimitar Dimitrov, and Martin Vechev. 2024. Modular Synthesis of Efficient Quantum Uncomputation.Proc. ACM Program. Lang.8, OOPSLA2, Article 345 (Oct. 2024), 28 pages. doi:10.1145/3689785

    2024 doi

  37. [45]

    Wille, D

    R. Wille, D. Große, L. Teuber, G. W. Dueck, and R. Drechsler. 2008. RevLib: An Online Resource for Reversible Functions and Reversible Circuits. InInt’l Symp. on Multi-Valued Logic. 220–225. RevLib is available at http://www.revlib.org

    2008

  38. [46]

    Dueck, and Rolf Drechsler

    Robert Wille, Daniel Große, Lisa Teuber, Gerhard W. Dueck, and Rolf Drechsler. 2008. RevLib: An Online Resource for Reversible Functions and Reversible Circuits. In38th International Symposium on Multiple Valued Logic (ISMVL 2008). 220–225. doi:10.1109/ISMVL.2008.43

    2008 doi

  39. [47]

    2024.Foundations of quantum programming

    Mingsheng Ying. 2024.Foundations of quantum programming. Second Edition. Morgan Kaufmann

    2024

  40. [48]

    Zhicheng Zhang, Qisheng Wang, and Mingsheng Ying. 2024. Parallel Quantum Algorithm for Hamiltonian Simulation. Quantum8 (Jan. 2024), 1228. doi:10.22331/q-2024-01-15-1228

    2024 doi

  41. [49]

    Ben Zindorf and Sougato Bose. 2025. Efficient implementation of multicontrolled quantum gates.Phys. Rev. Appl.24 (Oct 2025), 044030. Issue 4. doi:10.1103/8blx-nfcr Bona: Automatic Management of Dirty Ancilla Borrowing in Quantum Circuits 29 Supplementary Material A Proof of Pr...

    2025 doi

  42. [51]

    Case𝐶=𝑈[ 𝑝].This follows directly from Definition 3.2 and the definition of substituition: J𝑈[𝑝] K[𝑞/𝑑]=(𝑈 𝑝)[𝑞/𝑑]=𝑈 𝑝[𝑞/𝑑] = r 𝑈[𝑝[𝑞/𝑑]] z = J𝑈[𝑝][𝑞/𝑑] K

  43. [52]

    Case𝐶=𝐶 1;𝐶 2.Using the induction hypothesis: J(𝐶1;𝐶 2)[𝑑/𝑞] K = J(𝐶1[𝑑/𝑞]);𝐶 2[𝑑/𝑞] K = J𝐶2[𝑑/𝑞] K J𝐶1[𝑑/𝑞] K = J𝐶2K[𝑑/𝑞] J𝐶1K[𝑑/𝑞] =( J𝐶2K J𝐶1K)[𝑑/𝑞] = J𝐶1;𝐶 2K[𝑑/𝑞]

  44. [53]

    (a) If𝑑=𝑎.Then substitution does not affect the borrow binder: Jborrow[𝑎]{𝐶′}[𝑞/𝑑] K = Jborrow[𝑎]{𝐶′}K =𝐹 qv(𝐶′)\𝑎 =𝐹 qv(𝐶′)\𝑎[𝑞/𝑎], or both sides equal⊥if the borrow is unsafe

    Case𝐶=borrow[𝑎]{𝐶 ′}.We distinguish several subcases depending on the relationship among 𝑎,𝑞,𝑑. (a) If𝑑=𝑎.Then substitution does not affect the borrow binder: Jborrow[𝑎]{𝐶′}[𝑞/𝑑] K = Jborrow[𝑎]{𝐶′}K =𝐹 qv(𝐶′)\𝑎 =𝐹 qv(𝐶′)\𝑎[𝑞/𝑎], or both sides equal⊥if the borrow is unsafe. (b)...

  45. [54]

    It then adds two new edges: (𝑢,fst(𝑑)) and(lst(𝑑),𝑣)

    Balanced Condition.The splicing operation 𝐺[𝑒⊳𝑑] removes the boundary nodes In(𝑑) and Out(𝑑) , and the edges𝑒=(𝑢,𝑣) ,(In(𝑑),fst(𝑑)) , and(lst(𝑑),Out(𝑑)) . It then adds two new edges: (𝑢,fst(𝑑)) and(lst(𝑑),𝑣) . For any operation node𝑤∈𝑉 ′ =𝑉\{In(𝑑),Out(𝑑)} , its degree changes ...

  46. [55]

    Furthermore, as shown in the proof balanced condition, no degree of the nodes changes

    I/O Consistency.Because 𝑑 and its boundary nodes, In(𝑑) and Out(𝑑) , are entirely removed from the updated sets𝑄′ and𝑉′, every remaining qubit𝑞∈𝑄 ′ still retains its respective In and Out nodes in𝑉′. Furthermore, as shown in the proof balanced condition, no degree of the nodes...

  47. [56]

    Because the original graph𝐺 is acyclic,𝐶𝑐𝑦𝑐𝑙𝑒 must utilize at least one of the newly added edges in𝐺′:(𝑢,fst(𝑑))or(lst(𝑑),𝑣)

    Acyclicity.Assume for the sake of contradiction that the unreachable condition holds, but 𝐺′ contains a cycle𝐶𝑐𝑦𝑐𝑙𝑒 . Because the original graph𝐺 is acyclic,𝐶𝑐𝑦𝑐𝑙𝑒 must utilize at least one of the newly added edges in𝐺′:(𝑢,fst(𝑑))or(lst(𝑑),𝑣). We analyze the three possible cas...

  48. [2020]

    In Proceedings of the ACM/IEEE 47th Annual International Symposium on Computer Architecture(Virtual Event)(ISCA ’20)

    SQUARE: strategic quantum ancilla reuse for modular quantum programs via cost-effective uncomputation. In Proceedings of the ACM/IEEE 47th Annual International Symposium on Computer Architecture(Virtual Event)(ISCA ’20). IEEE Press, 570–583. doi:10.1109/ISCA45697.2020.00054

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.