Pith. sign in

REVIEW 1 major objections 9 minor 37 references

Optimal CNOT and phase-polynomial circuits can be found by enumerating undirected gate topologies and deciding directions with semi-tensor-product factorization, in parallel and with far less overhead than SAT encoding on small shards.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-31 21:15 UTC pith:MJH3FJQL

load-bearing objection Solid quantum-compilation engineering: undirected topologies + STP direction factorization is a real third route beside SAT and databases, with honest parallel and portfolio numbers; one phase-poly exhaustiveness gap is the main soft spot. the 1 major comments →

arxiv 2607.24195 v1 pith:MJH3FJQL submitted 2026-07-27 quant-ph cs.ET

Parallelizable Exact Synthesis of Quantum Circuits via Semi-Tensor Product

Chenjian Li , Dingchao Gao , Xiangzhen Zhou , Ji Guan , Pengcheng Zhu , Zhufei Chu This is my paper
classification quant-ph cs.ET
keywords quantum circuit synthesisexact synthesissemi-tensor productCNOT circuitsphase polynomial circuitstopology enumerationparallel synthesiscircuit optimization
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Exact synthesis of small quantum circuit pieces is valuable for compilers, but SAT encodings carry heavy overhead and scale poorly in parallel, while circuit databases blow up in memory. This paper argues that CNOT (and CNOT-plus-phase) synthesis can instead be split into two independent stages: first enumerate undirected partial-gate topologies as circuit skeletons, then decide each gate’s control and target by converting the skeleton into canonical semi-tensor-product formulas and factorizing them right to left, pruning impossible direction assignments. Topology filters based on variable support and information-flow rank bounds keep the enumeration tractable, and the same skeleton idea extends to phase-polynomial circuits by requiring parity checkpoints. On random targets the method is typically two to three orders of magnitude faster than a SAT baseline on small instances and still competitive on harder ones; with many workers it reaches up to about 12.8× parallel speedup. Embedded as a peephole resynthesis kernel on real benchmark circuits, alone or in a portfolio with SAT, it wins on most cases with roughly 1.9× median end-to-end speedup.

Core claim

The authors establish that exact, gate-optimal synthesis of linear CNOT circuits—and, via checkpoint post-selection, of phase-polynomial circuits—can be performed by a two-stage procedure: breadth-first enumeration of undirected partial-gate topologies with safe pruning, followed by a native right-to-left STP factorization that retains only direction assignments realizing the target parity matrices. Because topologies are independent, both stages parallelize with little coordination, yielding large practical speedups over SAT encoding on the small-window instances that matter for compiler peephole rewriting.

What carries the argument

Canonical semi-tensor-product (STP) formulas for a topology’s outputs, decided by right-to-left factorization: each rightmost factor is peeled from the target structural matrix; swap and power-reduce factors always factor, while each undetermined partial gate branches on CT versus TC and drops directions that fail to factor. Topology pruning by support mismatch and bipartition rank lower bounds (plus checkpoint set-cover bounds for phase polynomials) cuts the exponential skeleton space before solving.

Load-bearing premise

The pruning rules and the factorization procedure must never discard a topology or direction set that could still implement the target; if either filter is incomplete, claimed optimality or completeness fails.

What would settle it

Construct a small linear target and a topology that implements it under some gate directions, yet is either pruned by the support/rank/checkpoint bounds or marked UNSAT by the factorization routine; a single such counterexample would break soundness of the exact kernel.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Compiler peephole passes can swap in an STP exact kernel for small CNOT or CNOT+Rz shards instead of relying only on SAT or precomputed databases.
  • Coarse-grained parallelism across topologies becomes a practical lever on multicore machines for this NP-hard subproblem, unlike many parallel SAT setups.
  • Phase-polynomial fragments common in QPE, QAOA, and VQE-style circuits become exact-resynthesis targets under the same skeleton-plus-checkpoint workflow.
  • An STP+SAT portfolio under a fixed worker budget can keep most of the speed win while covering instances where pure STP stalls.

Where Pith is reading between the lines

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

  • Tighter, solver-native encoding of parity checkpoints (instead of post-selection) could shrink the phase-polynomial search further without losing optimality.
  • The same undirected-topology plus algebraic-factorization split may transfer to other linear or affine reversible gate sets beyond CNOT.
  • Reusable factorization state across topologies that share prefixes could cut redundant work in deep enumerations.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

1 major / 9 minor

Summary. The paper proposes a two-stage exact synthesis framework for CNOT and CNOT+Rz (phase polynomial) circuits based on the semi-tensor product (STP) calculus. In the first stage, undirected "partial-gate" topologies (qubit-pair skeletons with unresolved control/target directions) are enumerated in BFS order of gate count and pruned by three lower-bound rules (variable mismatch, Eq. 49; bipartition rank, Eq. 55; checkpoint set-cover, Eqs. 57–58). In the second stage, each surviving topology is converted to canonical STP formulas and a right-to-left factorization procedure (FACTORIZE, Alg. 2) decides which direction assignments can realize the target structural matrices. The framework parallelizes across topologies and is evaluated against Qiskit-SAT (Z3) and a Gimsatul-backed parallel SAT configuration on random (n,g) grids and on 96 QASMBench circuits in a shard-based peephole workflow, reporting typical 100–1000× speedups on small instances, up to 12.8× parallel speedup on 32 workers, and a median 1.91× end-to-end speedup for an STP+SAT portfolio.

Significance. If the optimality argument is repaired, this is a useful addition to the exact-synthesis toolbox: a third route besides SAT encodings and precomputed databases, with measured (not fitted) speedups against external baselines (Qiskit-SAT/Z3, Gimsatul), demonstrated coarse-grained parallel scalability (up to 12.8× on 32 workers, exceeding the parallel SAT backend on the same instances), and an end-to-end peephole evaluation on 96 QASMBench circuits with a same-budget parallel baseline and a sensible portfolio fallback. The pruning rules are provably safe lower bounds rather than heuristics that compromise exactness. The claimed niche — a lightweight exact kernel for small-to-moderate shards embedded in larger workflows — is well supported by the experiments and is realistically scoped. The paper does not ship machine-checked proofs or a public artifact, which limits independent verification of the implementation-level claims.

major comments (1)
  1. The optimality claim for the phase-polynomial mode is not established by the algorithm as written. SOLVE returns D as a pooled set of direction assignments (Alg. 1 line 27 initializes D = {CT,TC}^#g, and FACTORIZE intersects/unions these sets), but Alg. 3 line 11 performs C ← INSTANTIATE(T, D), producing a single circuit, and line 12 checks checkpoint coverage only on that one instantiation. Checkpoint coverage is instantiation-dependent: two direction assignments in D realize the same final parity matrix A but generally produce different intermediate wire parities, so a topology whose checkpoint coverage holds only under some completions in D can be discarded if INSTANTIATE picks a non-covering one. In that case the search finds no solution at the minimal #g and proceeds to #g+1, silently returning a non-optimal result. The one-sentence justification ('Since gate counts are considered[*
minor comments (9)
  1. [Sec. IV] Sec. IV, first paragraph of the algorithm description: 'uses the STP synthesis algorithm introduced in Sec. 1' — should be Sec. III.
  2. [Sec. III-A] Sec. III-A, after Eq. (35): 'and x is participate in the expression in their vector form' — typographical error; please revise the sentence.
  3. [Abstract / Sec. V-C] The median speedup is quoted as 1.88× in the Introduction and Sec. V-C but as 1.9× in Table II, and the abstract's '89% of cases' corresponds to the portfolio (85/96) while the Introduction quotes 75/96 for pure STP — where the denominator is actually the 94 completed instances. Please state denominators and round consistently.
  4. [Sec. V-A] Fig. 2 and Sec. V-A: it is not stated how timed-out runs enter the per-configuration averages (counted as 600 s? excluded?). This matters for interpreting the '100–1000×' speedup claim in the abstract; please specify, and consider reporting medians or per-instance scatter given only 10 samples per (n,g).
  5. [Sec. V-B] Sec. V-B refers to supplementary material for speedups at smaller worker counts, but no supplement accompanies the arXiv submission; please include it or upload it with the revision.
  6. [Sec. V-C] Sec. V-C: the shard-selection heuristic h(A) is described only as 'a heuristic that predicts the minimal number of CNOT gates required to implement A.' Please define how h is computed (it affects reproducibility of the workflow even though it does not affect exactness of the shards).
  7. [Alg. 1] Alg. 1, Ensure clause: 'Optimal CNOT circuit(s)' suggests all optimal circuits are returned, but line 9 adds one instantiation per feasible topology. Please clarify whether the algorithm returns one optimal circuit per topology or exhausts D, and align the Ensure clause.
  8. [Sec. II-A / Sec. III-A] Please state the parity-matrix convention once (e.g., Eq. (10) and CNOT_{1,2} ~ [[1,0],[1,1]] imply output-vector = A·input-vector with target row receiving the control row); this would help readers connect Eq. (44)–(45) with the STP structural matrices M_i.
  9. [Sec. III-C] Table I caption mentions 'topology solving and pruning techniques,' but the table concerns pruning only.

Circularity Check

0 steps flagged

No significant circularity: algorithmic exact-synthesis claims are measured against external SAT/QASMBench baselines, not defined into existence by fitted parameters or load-bearing self-citation.

full rationale

This is an algorithms-and-systems paper whose central claims are (i) a two-stage topology-enumeration + STP-factorization procedure for exact CNOT/phase-polynomial synthesis, (ii) soundness of stated pruning over-approximations, and (iii) wall-clock speedups versus Qiskit-SAT/Z3, Gimsatul, and a QASMBench peephole workflow. None of these reduce by construction to their inputs: runtimes and win-rates are empirical comparisons to independent solvers and public benchmarks; optimality is argued from BFS over increasing gate count plus (claimed) complete direction search, not from a quantity fitted on the same data being re-labeled as a prediction. STP canonical-form rewrite rules and factorization are standard algebraic machinery applied to circuit structure, not a self-definitional loop. The citation to Pan and Chu on classical STP logic synthesis is ordinary prior-work lineage (one co-author overlap) and is not used as a uniqueness theorem that forces the quantum results. Workflow knobs such as h(A)≤H=6 and two IBO rounds bound end-to-end quality but are not circular predictions. Completeness worries about INSTANTIATE/D (whether every feasible direction set is checkpoint-checked) are correctness risks, not circularity. Score 0; steps empty.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 2 invented entities

The work rests on standard finite-field linear algebra for CNOT circuits, the established phase-polynomial/skeleton-checkpoint model, and Cheng’s STP calculus, plus engineering thresholds in the optimizer workflow. No new physical entities; free parameters are compiler heuristics and parallel budgets rather than fitted physical constants.

free parameters (4)
  • shard complexity threshold H = 6
    Longest prefix with heuristic score h(A)≤H is taken as a shard; H is set to 6 by hand to sit beyond typical permutation-free databases while remaining solvable.
  • IBO rounds and window constraints = 2 rounds; ≥30 gates/side
    Up to two iterative blockwise optimization rounds; windows must pull ≥30 gates from each side of a boundary and still satisfy h(A)≤H—policy choices that affect end-to-end wins.
  • parallel worker budget / portfolio split = 32; portfolio 16+16
    Speedups reported at 32 workers; portfolio uses 16 STP + 16 Gimsatul under the same total budget—experimental configuration, not derived.
  • random-instance sample size and timeout = 10 per cell; 600s / 3600s
    10 random circuits per (n,g) cell; 600 s synthesis timeout and 3600 s workflow timeout shape averaged curves and win rates.
axioms (6)
  • domain assumption n-qubit CNOT circuits are exactly the invertible linear maps A∈GL(n,2) acting on parity vectors over F2.
    Used throughout Sec. II–III as the synthesis target representation.
  • standard math Semi-tensor product with structural matrices, swap Mw, and power-reduce Mr can represent and canonicalize the Boolean/linear action of partial CNOT topologies (Cheng STP theory).
    Sec. II-B; factorization completeness inherits from this representation.
  • domain assumption Phase-polynomial unitaries of the stated sum-over-paths form are realized by a CNOT skeleton hitting every required parity checkpoint, then placing Rz rotations.
    Sec. II-A and IV following Amy et al.; reduces phase synthesis to constrained CNOT skeletons.
  • ad hoc to paper BFS increasing partial-gate count yields CNOT-count-optimal solutions if every topology at the minimal feasible count is considered (modulo sound pruning) and SOLVE is complete.
    Alg. 1 optimality argument in Sec. III; depends on pruning safety and factorization completeness.
  • ad hoc to paper Each additional partial gate resolves at most one variable-mismatch output; cross-partition partial gates are lower-bounded by rank(A_Q1Q2)+rank(A_Q2Q1).
    Sec. III-C pruning; correctness of search-space reduction rests on these combinatorial bounds.
  • ad hoc to paper Checkpoint reachability can be safely under-approximated via set-cover bounds on supports for pruning (Eq. cover_q / max min cover).
    Sec. IV; authors note the bound is optimistic and ignore directions/sharing.
invented entities (2)
  • Undirected partial-gate topology with separate CT/TC direction variables independent evidence
    purpose: Expose independent skeletons for parallel enumeration and STP direction solving
    Core modeling device of the framework (Sec. II-A, III); standard EDA-style partial gates adapted to CNOT.
  • Right-to-left STP factorization circuit solver (FACTORIZE) no independent evidence
    purpose: Decide which direction assignments realize target structural matrices without SAT encoding
    Native solver in Alg. 2; analogous to classical STP exact synthesis but specialized to CNOT factors.

pith-pipeline@v1.2.0-grok45-kimik3 · 23964 in / 3994 out tokens · 80850 ms · 2026-07-31T21:15:32.265518+00:00 · methodology

0 comments
read the original abstract

Exact synthesis is a useful tool in quantum compilation by providing optimal alternative implementations of small circuit shards and is widely used as a circuit re-synthesis optimization kernel. However, existing exact synthesis methods suffer from encoding overhead, poor parallel scalability, and memory bottlenecks. This paper introduces a parallel exact synthesis framework for CNOT and phase polynomial circuits, which is based on the semi-tensor product (STP) theory of matrices. By enumerating undirected partial-gate topologies and solving the missing gate directions separately, we are able to parallelize both stages and achieve a parallel speedup of up to $12.8\times$ with 32 workers on this NP-hard problem. More specifically, for each topology, the circuit semantics are converted into canonical STP formulas, and feasibility is decided by a right-to-left factorization procedure that removes infeasible direction assignments. On randomly generated synthesis targets, STP is typically $100\times-1000\times$ faster than the SAT-based baseline on small instances, and remains competitive for more difficult instances. When integrated in a real-world circuit optimization workflow, our algorithm outperforms the SAT-based approach on 89% of cases in QASMBench, and achieves a median speedup of $1.91\times$.

Figures

Figures reproduced from arXiv: 2607.24195 by Chenjian Li, Dingchao Gao, Ji Guan, Pengcheng Zhu, Xiangzhen Zhou, Zhufei Chu.

Figure 1
Figure 1. Figure 1: Overall structure of our STP-based synthesis algorithm for a fixed gate count ( [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Runtime of STP against Qiskit-SAT on random CNOT circuits. For each data point, 10 random circuits are generated and tested. The timeout value [PITH_FULL_IMAGE:figures/full_fig_p010_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Parallel speedup of STP against Qiskit-SAT with the Gimsatul backend [ [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Optimization runtime of Gimsatul, STP and STP+Gimsatul portfolio on QASMBench. Left: QASMBench cases with gate count smaller than 100; [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Speedup of STP-based kernels over Gimsatul on different categories [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗

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

37 extracted references · 4 linked inside Pith

  1. [1]

    Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer,

    P. W. Shor, “Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer,”SIAM review, vol. 41, no. 2, pp. 303–332, 1999

    1999

  2. [2]

    Quantum mechanics helps in searching for a needle in a haystack,

    L. K. Grover, “Quantum mechanics helps in searching for a needle in a haystack,”Physical review letters, vol. 79, no. 2, p. 325, 1997

    1997

  3. [3]

    Quantum Algorithm for Linear Systems of Equations,

    A. W. Harrow, A. Hassidim, and S. Lloyd, “Quantum Algorithm for Linear Systems of Equations,”Physical Review Letters, vol. 103, no. 15, p. 150502, Oct. 2009

    2009

  4. [4]

    Quantum Circuits for General Multiqubit Gates,

    M. M ¨ott¨onen, J. J. Vartiainen, V . Bergholm, and M. M. Salomaa, “Quantum Circuits for General Multiqubit Gates,”Physical Review Letters, vol. 93, no. 13, p. 130502, Sep. 2004

    2004

  5. [5]

    Synthesis of Quan- tum Logic Circuits,

    V . V . Shende, S. S. Bullock, and I. L. Markov, “Synthesis of Quan- tum Logic Circuits,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 25, no. 6, pp. 1000–1010, Jun. 2006

    2006

  6. [6]

    Practical exact synthesis,

    M. Soeken, W. Haaswijk, E. Testa, A. Mishchenko, L. G. Amaru, R. K. Brayton, and G. De Micheli, “Practical exact synthesis,” in2018 Design, Automation & Test in Europe Conference & Exhibition (DATE). Dresden, Germany: IEEE, Mar. 2018, pp. 309–314

    2018

  7. [7]

    ” Non-identity-check

    D. Janzing, P. Wocjan, and T. Beth, “” Non-identity-check” is QMA- complete,”International Journal of Quantum Information, vol. 3, no. 03, pp. 463–473, 2005

    2005

  8. [8]

    On the CNOT-complexity of CNOT-PHASE circuits,

    M. Amy, P. Azimzadeh, and M. Mosca, “On the CNOT-complexity of CNOT-PHASE circuits,”Quantum Science and Technology, vol. 4, no. 1, p. 015002, Sep. 2018

    2018

  9. [9]

    Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation,

    I. Shaik and J. van de Pol, “Optimal Layout-Aware CNOT Circuit Synthesis with Qubit Permutation,” Aug. 2024

    2024

  10. [10]

    HOPPS: Hardware- Aware Optimal Phase Polynomial Synthesis with Blockwise Optimiza- tion for Quantum Circuits,

    X. Li, J. Liu, S. Xu, P. Hovland, and V . Chaudhary, “HOPPS: Hardware- Aware Optimal Phase Polynomial Synthesis with Blockwise Optimiza- tion for Quantum Circuits,” Nov. 2025

    2025

  11. [11]

    Heuristic and Optimal Synthesis of CNOT and Clifford Circuits,

    M. Webster, S. Koutsioumpas, and D. E. Browne, “Heuristic and Optimal Synthesis of CNOT and Clifford Circuits,” Mar. 2025

    2025

  12. [12]

    On Exact Sizes of Minimal CNOT Circuits,

    J. E. Christensen, S. F. Jørgensen, A. Pavlogiannis, and J. Van De Pol, “On Exact Sizes of Minimal CNOT Circuits,” inReversible Compu- tation, R. Gl ¨uck and R. Kaarsgaard, Eds. Cham: Springer Nature Switzerland, 2025, vol. 15716, pp. 71–88

    2025

  13. [13]

    An overview of parallel SAT solving,

    R. Martins, V . Manquinho, and I. Lynce, “An overview of parallel SAT solving,”Constraints, vol. 17, no. 3, pp. 304–347, 2012

    2012

  14. [14]

    Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers,

    G. Katsirelos, A. Sabharwal, H. Samulowitz, and L. Simon, “Resolution and parallelizability: Barriers to the efficient parallelization of SAT solvers,” inProceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, 2013, pp. 481–488

    2013

  15. [15]

    Cheng, H

    D. Cheng, H. Qi, and Y . Zhao,An Introduction to Semi-Tensor Product of Matrices and Its Applications. WORLD SCIENTIFIC, Jul. 2012

    2012

  16. [16]

    Quantum measurements and the abelian stabilizer prob- lem,

    A. Y . Kitaev, “Quantum measurements and the abelian stabilizer prob- lem,”arXiv preprint quant-ph/9511026, 1995

    Pith/arXiv arXiv 1995

  17. [17]

    A Quantum Approximate Optimization Algorithm,

    E. Farhi, J. Goldstone, and S. Gutmann, “A Quantum Approximate Optimization Algorithm,” Nov. 2014

    2014

  18. [18]

    A variational eigenvalue solver on a photonic quantum processor,

    A. Peruzzo, J. McClean, P. Shadbolt, M.-H. Yung, X.-Q. Zhou, P. J. Love, A. Aspuru-Guzik, and J. L. O’brien, “A variational eigenvalue solver on a photonic quantum processor,”Nature communications, vol. 5, no. 1, p. 4213, 2014

    2014

  19. [19]

    Qasmbench: A low- level quantum benchmark suite for nisq evaluation and simulation,

    A. Li, S. Stein, S. Krishnamoorthy, and J. Ang, “Qasmbench: A low- level quantum benchmark suite for nisq evaluation and simulation,”ACM Transactions on Quantum Computing, vol. 4, no. 2, pp. 1–26, 2023

    2023

  20. [20]

    Optimal synthesis of linear reversible circuits,

    K. Patel, I. Markov, and J. Hayes, “Optimal synthesis of linear reversible circuits,”Quantum Information and Computation, vol. 8, no. 3&4, pp. 282–294, Mar. 2008

    2008

  21. [21]

    Quantum computing and polynomial equations over the finite field z 2,

    C. M. Dawson, H. L. Haselgrove, A. P. Hines, D. Mortimer, M. A. Nielsen, and T. J. Osborne, “Quantum computing and polynomial equations over the finite field z 2,”arXiv preprint quant-ph/0408129, 2004

    Pith/arXiv arXiv 2004

  22. [22]

    Quantum circuits and low-degree polynomials over f 2,

    A. Montanaro, “Quantum circuits and low-degree polynomials over f 2,” arXiv preprint arXiv:1607.08473, 2016

    Pith/arXiv arXiv 2016

  23. [23]

    Phasepoly: An optimization framework forphase polynomials in quantum circuits,

    Z. Chen, H. Chen, Y . Jin, M. Guo, E. Jang, J. Li, C. Chan, W. W. Ro, and E. Z. Zhang, “Phasepoly: An optimization framework forphase polynomials in quantum circuits,”arXiv preprint arXiv:2506.20624, 2025

    Pith/arXiv arXiv 2025

  24. [24]

    Polynomial-time T-depth optimiza- tion of Clifford+ T circuits via matroid partitioning,

    M. Amy, D. Maslov, and M. Mosca, “Polynomial-time T-depth optimiza- tion of Clifford+ T circuits via matroid partitioning,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 33, no. 10, pp. 1476–1489, 2014

    2014

  25. [25]

    Towards Optimal Topology Aware Quantum Circuit Synthesis,

    M. G. Davis, E. Smith, A. Tudor, K. Sen, I. Siddiqi, and C. Iancu, “Towards Optimal Topology Aware Quantum Circuit Synthesis,” in2020 IEEE International Conference on Quantum Computing and Engineer- ing (QCE). Denver, CO, USA: IEEE, Oct. 2020, pp. 223–234

    2020

  26. [26]

    A computing procedure for quantification theory,

    M. Davis and H. Putnam, “A computing procedure for quantification theory,”Journal of the ACM (JACM), vol. 7, no. 3, pp. 201–215, 1960

    1960

  27. [27]

    A machine program for theorem-proving,

    M. Davis, G. Logemann, and D. Loveland, “A machine program for theorem-proving,”Communications of the ACM, vol. 5, no. 7, pp. 394– 397, 1962

    1962

  28. [28]

    qiskit-sat-synthesis,

    A. Ivrii and M. Treinish, “qiskit-sat-synthesis,” 2021, accessed: 2025-11-16. [Online]. Available: https://github.com/qiskit-community/ qiskit-sat-synthesis

    2021

  29. [29]

    Scalable proof-producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses,

    M. Fleury and A. Biere, “Scalable proof-producing multi-threaded SAT solving with Gimsatul through sharing instead of copying clauses,” 2022

    2022

  30. [30]

    Atomique: A quantum compiler for reconfigurable neutral atom arrays,

    H. Wang, P. Liu, D. B. Tan, Y . Liu, J. Gu, D. Z. Pan, J. Cong, U. A. Acar, and S. Han, “Atomique: A quantum compiler for reconfigurable neutral atom arrays,” in2024 ACM/IEEE 51st Annual International Symposium on Computer Architecture (ISCA). IEEE, 2024, pp. 293–309

    2024

  31. [31]

    Compiling quantum circuits for dynamically field-programmable neutral atoms array processors,

    D. B. Tan, D. Bluvstein, M. D. Lukin, and J. Cong, “Compiling quantum circuits for dynamically field-programmable neutral atoms array processors,”Quantum, vol. 8, p. 1281, 2024

    2024

  32. [32]

    Quantum virtual ma- chines,

    R. Tao, H. Zhu, J. Nieh, J. Yao, and R. Gu, “Quantum virtual ma- chines,” in19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 25), 2025, pp. 411–428

    2025

  33. [33]

    Efficient decom- position of quantum gates,

    J. J. Vartiainen, M. Mottonen, and M. M. Salomaa, “Efficient decom- position of quantum gates,”Physical Review Letters, vol. 92, no. 17, p. 177902, Apr. 2004

    2004

  34. [34]

    Quantum circuits for isometries,

    R. Iten, R. Colbeck, I. Kukuljan, J. Home, and M. Christandl, “Quantum circuits for isometries,”Physical Review A, vol. 93, no. 3, p. 032318, 2016

    2016

  35. [35]

    Quantum-state preparation with universal gate decompositions,

    M. Plesch and C. Brukner, “Quantum-state preparation with universal gate decompositions,”Physical Review A—Atomic, Molecular, and Op- tical Physics, vol. 83, no. 3, p. 032302, 2011

    2011

  36. [36]

    Exact Synthesis Based on Semi-Tensor Product Circuit Solver,

    H. Pan and Z. Chu, “Exact Synthesis Based on Semi-Tensor Product Circuit Solver,” in2023 Design, Automation & Test in Europe Confer- ence & Exhibition (DATE). Antwerp, Belgium: IEEE, Apr. 2023, pp. 1–6

    2023

  37. [37]

    Linear-Time T-Gate Optimization via Random Ab- straction,

    A. Albarghouthi, “Linear-Time T-Gate Optimization via Random Ab- straction,” May 2026

    2026