Pith. sign in

REVIEW 4 major objections 4 minor 63 references

FeynmanDD computes quantum amplitudes by counting solutions on a decision diagram.

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 →

FeynmanDD maps Feynman path integral sums onto classical decision diagrams, so quantum circuit amplitudes, probabilities, and equivalence checks become BDD counting tasks that run very fast on structured circuits.

T0 review reviewed 2026-08-04 challenge →

load-bearing objection A real new combination of Feynman path sums and classical BDD counting, with impressive but not yet fully explained speedups; the deferred complexity analysis and missing code keep it conditional. the 4 major comments →

arxiv 2509.08276 v1 pith:67JJMIMV submitted 2025-09-10 quant-ph cs.DS

FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams

classification quant-ph cs.DS
keywords FeynmanDDbinary decision diagramsmulti-terminal BDDsum-of-powers representationquantum circuit simulationamplitude computationequivalence checkingvariable ordering
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.

The reading

FeynmanDD is a new classical simulation method that turns quantum circuit analysis into a counting problem. The paper shows that, for circuits built from discrete gate sets, the Feynman-path-integral expression for an amplitude can be written as a sum of powers of a root of unity, with the exponent a low-degree multilinear polynomial. That polynomial is compiled into a multi-terminal binary decision diagram, and the amplitude is recovered by counting how many assignments send the polynomial to each residue. The paper proves the evaluation runs in time linear in the diagram size, and reports that for structured families such as GHZ, BV, linear-network, and supremacy-benchmark circuits, the diagrams stay small enough to beat standard simulators by orders of magnitude. A reader should care because this opens a new route to classically simulating and verifying quantum circuits that exploits repetition in the circuit's algebraic form rather than in its state vector.

Core claim

The central claim is that one can map a quantum circuit to a sum-of-powers representation of the target amplitude—an expression 1/√R Σ_y ω^{f(x,y)} where ω is a root of unity and f is a multilinear polynomial of degree at most three—and then treat the circuit-analysis task as a counting problem over f. Given an MTBDD for f with B(f) nodes, FeynmanDD computes any amplitude exactly in O(mB(f)) time, where m is the counting bit length; the same machinery handles acceptance probabilities and, by forming the trace of U†V, equivalence checking. The paper constructs sum-of-powers forms for three universal gate sets—the H/Z/CZ/CCZ set, the Clifford+T set, and the supremacy-benchmark gate set—and pro

What carries the argument

The load-bearing object is the sum-of-powers form: a circuit gate is encoded as a power ω^{ℓ(x)} of a root of unity, so the whole circuit becomes a uniformly normalized sum over internal wire values, with the exponent a multilinear polynomial. The companion machinery is the multi-terminal binary decision diagram, a rooted directed acyclic graph whose leaves hold residue values, built for the exponent polynomial. Once the MTBDD exists, evaluation of the sum-of-powers form is a residue-counting problem: count assignments yielding each residue and combine with the roots of unity, in time linear in the diagram size. Two ordering choices carry the method: the order in which polynomial terms are a

Load-bearing premise

The method's speed collapses if the circuit's exponent polynomial cannot be squeezed into a small decision diagram; the paper's experiments depend on variable-ordering heuristics to keep the diagram small, and it defers a formal characterization of when that is possible.

What would settle it

Instrument the implementation to record the MTBDD node count B(f) and runtime for amplitudes on the published benchmark circuits; if runtime is not proportional to B(f) up to the counting bit length, the claimed linear-in-B(f) guarantee is not what the implementation delivers. Alternatively, run it on random layers of CCZ gates and check whether the diagram size and runtime grow exponentially with qubit count despite trying each ordering heuristic the paper suggests; that would demarcate the method's practical boundary.

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

If this is right

  • Single-amplitude simulation becomes as easy as the diagram is small: any circuit whose sum-of-powers polynomial admits a polynomially sized MTBDD is simulable in polynomial time, independent of entanglement structure.
  • Sampling by sequential conditional probabilities is available on the same diagram, with a quadratic cost in diagram size, so structured circuits can be sampled without storing the full state.
  • Equivalence checking can be done exactly via the trace criterion, using the same counting engine, and the paper reports fast checks on large GHZ and BV circuits.
  • Adding a new gate set requires only a configuration-file entry for the gate's power form, not a new data structure, so the method extends to other discrete universal sets.
  • The existence of a circuit family where FeynmanDD is efficient while tensor-network and Clifford methods are provably costly suggests BDD counting captures structure those methods miss.

Where Pith is reading between the lines

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

  • Editorial inference: if polynomially sized sum-of-powers BDDs exist for a broad class of circuits, the method effectively characterizes a new classical-simulability region defined by low XOR-treewidth of the path-sum polynomial, rather than by stabilizer rank or tensor-network cutwidth.
  • Editorial inference: the variable-ordering bottleneck suggests a direct test: run FeynmanDD on random constant-depth IQP circuits with many CCZ gates under sifting and tensor-order heuristics; if diagrams blow up polynomially with qubit count, the practical reach extends well beyond the tested families.
  • Editorial inference: the trace-based equivalence check could be combined with circuit optimizers to validate whole compiled programs exactly; a concrete extension is to benchmark on large Clifford+T circuits produced by rotation synthesis, where the paper only sketches the expected BDD behavior.
Share X Bluesky LinkedIn Reddit HN

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

4 major / 4 minor

Summary. The paper proposes FeynmanDD, a decision-diagram method for exact simulation and equivalence checking of quantum circuits over discrete gate sets. The method derives a sum-of-powers (SOP) representation of an amplitude or trace, converts the associated multilinear polynomial over Z_r into an MTBDD, and evaluates the amplitude by counting how many assignments map to each residue. Sections 3--4 give the SOP calculus for gate sets Z, T, and the Google-supremacy set G, including contraction and substitution operations. Section 5 describes a binary synthesis construction and variable-ordering heuristics. Section 6 gives formulas for amplitudes, probabilities, sampling, and equivalence checking via tr(U_C0^dag U_C1). Section 7 reports speedups over DDSIM, SliQSim, and WCFLOBDD on Google-supremacy, GHZ, BV, and especially 'linear-network' circuits; Section 8 compares equivalence checking with MQT-QCEC. The paper states that amplitude simulation is linear in B(f), where B(f) is the MTBDD size, but explicitly defers a formal complexity characterization of the linear-network family to future work.

Significance. If the claimed runtime bounds held with polynomial B(f) for the tested families, FeynmanDD would be a genuinely interesting bridge between BDD counting and Feynman-path simulation: it would enable exact single-amplitude computation, exact sampling, and exact equivalence checking with very small memory on structured circuits. The SOP framework is flexible, the counting formulation is exact, and the paper gives clear Theorems 1--2 and explicit formulas in Section 6. These are strengths. However, the submitted manuscript does not prove that B(f) stays small for the headline families, and the only justification for the MTBDD-building phase is empirical ('numerical simulations suggest'). The significance is therefore conditional on the deferred complexity analysis and on the reproducibility of the experimental results. No machine-checked proofs or released code accompany the paper, so the empirical claims are not independently verifiable at this stage.

major comments (4)
  1. [§6.1 and §5] The claim 'our simulation algorithm achieves runtime linear in B(f)' is only established for the counting phase. The BDD construction, which Section 5 calls 'the most computationally expensive step', is justified by 'Numerical simulations suggest' for the binary synthesis method, with no bound on its time relative to B(f); variable ordering can change B(f) exponentially. Therefore the full pipeline's runtime is not shown to be linear in B(f). Please either provide a construction-time bound or restrict the claim to the counting stage and report construction versus counting times in the experiments.
  2. [§1, §7.3] The formal complexity of the method, and specifically of the linear-network family, is explicitly deferred: §1 says 'In a follow-up work, we will provide a characterization of the complexity', and §7.3 says 'A more comprehensive analysis of this circuit family will be presented in subsequent work.' Yet the linear-network circuits are 'purposefully' designed so that the number of forward signals is bounded by k+1. As submitted there is no theorem showing B(f) is polynomial for this family, so the extreme speedups in Table 6 are unexplained empirically; they could depend on the fixed qubit ordering. A scaling experiment in n and k with several orderings, or an actual theorem, is needed to support the claimed advantage over tensor-network and Clifford methods.
  3. [§5 and §7] The experimental protocol fixes the 'qubit order' variable ordering for all circuits. Section 5 states that variable ordering 'may significantly impact the final size' and exhibits an ordering that makes the Hadamard-chain BDD blow up exponentially. For the Google-supremacy results (Tables 2--3), no evidence is given that the speedups are robust with respect to variable ordering or circuit variation (e.g., neighboring grid sizes). Without this, the 0.01--0.2 s amplitude times could be artifacts of a single favorable ordering rather than a property of the circuits. Report results for at least two orderings, or provide a size analysis of B(f) for these circuits.
  4. [§7 (experimental setup)] No code, data, or detailed benchmark-generation scripts are released. Given that the performance claims rely entirely on the experimental tables, the absence of artifacts prevents independent reproduction. I ask the authors to release the FeynmanDD implementation, the exact circuit instances (including random seeds for GRCS and linear-network circuits), and the scripts used for the DDSIM/SliQSim/WCFLOBDD comparisons.
minor comments (4)
  1. [§6.1] The symbol m is used for the number of circuit gates earlier and for the bit length of the counting result in Section 6.1. Use different symbols (e.g., M for gate count, ℓ for bit length) to avoid confusion.
  2. [§5] The counting-identity paragraph contains a garbled phrase: 'when a variable x appears exactly twice in the terms having form r/2 x x0 and r/2 x x1'. Please rewrite the condition precisely (which monomials, which coefficients, and what simplification follows).
  3. [Tables 4--5] Typographical errors: 'meausred' for 'measured' in the captions of Tables 4 and 5. Also, the notation in Table 3's caption '(x)' should be explained more clearly in the table text.
  4. [§6.2] The equivalence criterion is stated as 'equivalent (up to a global phase)' when the trace has unit norm. Please spell out the argument briefly (all eigenvalues of a unitary are on the unit circle, so modulus 2^n forces them to coincide), and clarify the distinction between 'equal as unitaries' and 'equal up to a global phase'.

Circularity Check

0 steps flagged

No circularity: the runtime claim follows from standard BDD counting, and the deferred BDD-size characterization is an open-evidence gap, not a circular step.

full rationale

FeynmanDD's derivation chain is self-contained. The sum-of-powers (SOP) representation (Theorem 1) is constructed directly from gate matrix elements and the Feynman path sum; it does not presuppose the amplitudes or counts that the algorithm later outputs. Section 6.1's linear-in-B(f) runtime claim is a direct application of known BDD model-counting results (Knuth [31]; Wegener [58]): once f is represented as an MTBDD of size B(f), the counts N_j are obtained by counting paths, not by fitting any parameter to the target amplitude. No benchmark output is used to define the method, and no load-bearing conclusion rests on a self-citation. The experimental speedups are conditional on B(f) remaining small under the chosen qubit order; the paper explicitly flags this as an open question ('the tensor contraction complexity bound is an upper bound that may be very loose in certain cases', Section 5; 'A more comprehensive analysis of this circuit family will be presented in subsequent work', Section 7.3; 'In a follow-up work, we will provide a characterization of the complexity of the FeynmanDD method', Section 1). That is an unproven premise or evidence gap, not a circular reduction: the theoretical claim is conditional on B(f), and the empirical claims are observations on particular circuit families. The equivalence-checking criterion tr(U†V)=2^n ω^j is a standard mathematical fact, and the benchmarks (GRCS, RevLib, and the authors' own circuit families) are test inputs, not fitted parameters. No circular step can be exhibited from the paper's equations or citations, so the score is 0.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

No free parameters are fitted to data; the algorithm relies on standard BDD counting, explicit power-form gate representations, and the trace criterion. No new physical entities are introduced.

axioms (3)
  • standard math BDD counting algorithms compute the number of satisfying assignments in time linear in BDD size (Knuth TAOCP; Wegener).
    Section 2.3 and 6.1 rely on this to turn MTBDD into counts N_j.
  • domain assumption Gate sets Z, T, G admit sum-of-powers representations with roots of unity, e.g., H = sum over x,y of (-1)^{xy}/sqrt(2).
    Section 3 builds SOP forms on these explicit representations; Theorem 1 is summarized without full proof but follows by construction from the gate definitions.
  • standard math Two unitaries U and V are equivalent up to global phase iff tr(U^dag V) has magnitude 2^n.
    Section 6.2 reduces equivalence checking to evaluating this trace, relying on spectral properties of unitary matrices.

reviewed 2026-08-04 · how reviews work

0 comments
Cite this review

Pith. "Pith review of FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams." pith.science (2026). https://pith.science/paper/67JJMIMV

@misc{pith2026250908276,
  author       = {Pith},
  title        = {Pith review of: FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/67JJMIMV}},
  note         = {Machine review of arXiv:2509.08276}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Applications of decision diagrams in quantum circuit analysis have been an active research area. Our work introduces FeynmanDD, a new method utilizing standard and multi-terminal decision diagrams for quantum circuit simulation and equivalence checking. Unlike previous approaches that exploit patterns in quantum states and operators, our method explores useful structures in the path integral formulation, essentially transforming the analysis into a counting problem. The method then employs efficient counting algorithms using decision diagrams as its underlying computational engine. Through comprehensive theoretical analysis and numerical experiments, we demonstrate FeynmanDD's capabilities and limitations in quantum circuit analysis, highlighting the value of this new BDD-based approach.

Figures

Figures reproduced from arXiv: 2509.08276 by Bin Cheng, Longxiang Yuan, Zhengfeng Ji, Ziyuan Wang.

Figure 1
Figure 1. Figure 1: Left: Variable labeling for a quantum circuit of gates from gate set Z. Right: A decomposition that derives a power-of-sum representation for CNOT. The H gate has matrix entries (−1)xy/ √ 2 where x and y are the variables for the input and output wires respectively. The CCZ gate has diagonal entries of (−1)x1x2x3 with 0 entries elsewhere, using the same set of variables for the input and output to indicate… view at source ↗
Figure 2
Figure 2. Figure 2: BDD for the reduced func￾tion x4 + x5x6 + x4x6x7. For instance, in the example circuit on the left part of [PITH_FULL_IMAGE:figures/full_fig_p011_2.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

63 extracted references · 38 canonical work pages · 1 internal anchor

  1. [1]

    The- ory of Computing9(1), 143–252 (2013)

    Aaronson, S., Arkhipov, A.: The Computational Complexity of Linear Optics. The- ory of Computing9(1), 143–252 (2013). https://doi.org/10.4086/toc.2013.v009a004

  2. [2]

    Physical Review A70(5), 052328 (2004)

    Aaronson, S., Gottesman, D.: Improved Simulation of Stabilizer Circuits. Physical Review A70(5), 052328 (2004). https://doi.org/10.1103/PhysRevA.70.052328

  3. [3]

    In: Proceedings of the Design Automation & Test in Europe Conference

    Abdollahi, A., Pedram, M.: Analysis and Synthesis of Quantum Circuits by Using Quantum Decision Diagrams. In: Proceedings of the Design Automation & Test in Europe Conference. pp. 1–6. IEEE, Munich, Germany (2006). https://doi.org/10. 1109/date.2006.244176

  4. [4]

    Verifying Quantum Circuits with Level-Synchronized Tree Automata9(POPL), 32:923–32:953 (2025)

    Abdulla, P.A., Chen, Y.G., Chen, Y.F., Holík, L., Lengál, O., Lin, J.A., Lo, F.Y., Tsai, W.L.: Verifying Quantum Circuits with Level-Synchronized Tree Automata. Verifying Quantum Circuits with Level-Synchronized Tree Automata9(POPL), 32:923–32:953 (2025). https://doi.org/10.1145/3704868

  5. [5]

    Amy, M.: Formal Methods in Quantum Circuit Design. Ph.D. thesis, University of Waterloo (2019)

  6. [6]

    Electronic Proceedings in Theoretical Computer Science287, 1–21 (2019)

    Amy, M.: Towards Large-scale Functional Verification of Universal Quantum Cir- cuits. Electronic Proceedings in Theoretical Computer Science287, 1–21 (2019). https://doi.org/10.4204/EPTCS.287.1

  7. [7]

    Electronic Proceedings in Theoretical Computer Science384, 127–141 (2023)

    Amy, M.: Complete equational theories for the sum-over-paths with unbalanced amplitudes. Electronic Proceedings in Theoretical Computer Science384, 127–141 (2023). https://doi.org/10.4204/eptcs.384.8

  8. [8]

    Nature 574(7779), 505–510 (2019)

    Arute, F., Arya, K., Babbush, R., Bacon, D., Bardin, J.C., Barends, R., Biswas, R., Boixo, S., Brandao, F.G.S.L., Buell, D.A., Burkett, B., Chen, Y., Chen, Z., Chiaro, B., Collins, R., Courtney, W., Dunsworth, A., Farhi, E., Foxen, B., Fowler, A., Gidney, C., Giustina, M., Graff, R., Guerin, K., Habegger, S., Harrigan, M.P., Hart- mann, M.J., Ho, A., Hoff...

  9. [9]

    In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD)

    Bahar, R., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD). pp. 188–191. IEEE Comput. Soc. Press, Santa Clara, CA, USA (1993). https://doi.org/10.1109/iccad. 1993.580054

  10. [10]

    IEEE Transactions on ComputersC-35(8), 677–691 (1986)

    Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on ComputersC-35(8), 677–691 (1986). https://doi.org/10.1109/tc. 1986.1676819

  11. [11]

    In: Proceedings of IEEE International Conference on Computer Aided Design (ICCAD)

    Bryant, R.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: Proceedings of IEEE International Conference on Computer Aided Design (ICCAD). pp. 236–243. IEEE Comput. Soc. Press, San Jose, CA, USA (1995). https://doi.org/10.1109/iccad.1995.480018

  12. [12]

    In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE)

    Burgholzer, L., Bauer, H., Wille, R.: Hybrid Schrödinger-Feynman Simulation of Quantum Circuits With Decision Diagrams. In: 2021 IEEE International Conference on Quantum Computing and Engineering (QCE). pp. 199–206. IEEE, Broomfield, CO, USA (2021). https://doi.org/10.1109/QCE52317.2021.00037

  13. [13]

    Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Pro- gramming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxe...

  14. [14]

    In: Enea, C., Lal, A

    Chen, Y.F., Chung, K.M., Lengál, O., Lin, J.A., Tsai, W.L.: AutoQ: An Automata- Based Quantum Circuit Verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 139–153. Springer Nature Switzerland, Cham (2023). https://doi. org/10.1007/978-3-031-37709-9_7

  15. [15]

    In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I

    Coecke, B., Duncan, R.: Interacting Quantum Observables. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) Automata, Languages and Programming. pp. 298–310. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_25

  16. [16]

    Theoretical Computer Science897, 1–22 (2022)

    Coecke,B.,Horsman,D.,Kissinger,A.,Wang,Q.:Kindergardenquantummechanics graduates ...or how I learned to stop gluing LEGO together and love the ZX-calculus. Theoretical Computer Science897, 1–22 (2022). https://doi.org/10.1016/j.tcs.2021. 07.024

  17. [17]

    Dawson, C.: Solovay Kitaev algorithm (2019)

  18. [18]

    Quantum Info

    Dawson, C.M., Hines, A.P., Mortimer, D., Haselgrove, H.L., Nielsen, M.A., Os- borne, T.J.: Quantum computing and polynomial equations over the finite field Z2. Quantum Info. Comput.5(2), 102–112 (2005)

  19. [19]

    Deng, H., Tao, R., Peng, Y., Wu, X.: A case for synthesis of recursive quantum unitary programs. Proc. ACM Program. Lang.8(POPL) (2024). https://doi.org/ 10.1145/3632901

  20. [20]

    PhD, University of Twente, Enschede, The Netherlands (2016)

    van Dijk, T.: Sylvan: multi-core decision diagrams. PhD, University of Twente, Enschede, The Netherlands (2016). https://doi.org/10.3990/1.9789036541602

  21. [21]

    Proceedings of the Royal Society of London

    Fenner, S., Green, F., Homer, S., Pruim, R.: Determining acceptance possibility for a quantum computation is hard for the polynomial hierarchy. Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences455(1991), 3953–3966 (1999). https://doi.org/10.1098/rspa.1999.0485

  22. [22]

    Ferrara, A., Pan, G., Vardi, M.Y.: Treewidth in Verification: Local vs. Global. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. pp. 489–503. Lecture Notes in Computer Science, Springer, Berlin, Heidelberg (2005). https://doi.org/10.1007/11591191_34

  23. [23]

    International series in pure and applied physic, McGraw-Hill (1965)

    Feynman, R., Hibbs, A.: Quantum Mechanics and Path Integrals. International series in pure and applied physic, McGraw-Hill (1965)

  24. [24]

    Physical Review A87(3), 032332 (2013)

    Giles, B., Selinger, P.: Exact synthesis of multiqubit Clifford+ T circuits. Physical Review A87(3), 032332 (2013). https://doi.org/10.1103/physreva.87.032332

  25. [25]

    arXiv:quant-ph/9807006 (1998)

    Gottesman, D.: The Heisenberg Representation of Quantum Computers. arXiv:quant-ph/9807006 (1998)

  26. [26]

    ACM Transactions on Quantum Computing3(4), 22:1–22:21 (2022)

    Hillmich, S., Zulehner, A., Kueng, R., Markov, I.L., Wille, R.: Approximating Decision Diagrams for Quantum Circuit Simulation. ACM Transactions on Quantum Computing3(4), 22:1–22:21 (2022). https://doi.org/10.1145/3530776

  27. [27]

    In: 2022 IEEE/ACM International Conference On Computer Aided Design (ICCAD)

    Hong, X., Feng, Y., Li, S., Ying, M.: Equivalence Checking of Dynamic Quantum Circuits. In: 2022 IEEE/ACM International Conference On Computer Aided Design (ICCAD). pp. 1–8 (2022)

  28. [28]

    In: 2021 58th ACM/IEEE Design Automation Conference (DAC)

    Hong, X., Ying, M., Feng, Y., Zhou, X., Li, S.: Approximate Equivalence Checking of Noisy Quantum Circuits. In: 2021 58th ACM/IEEE Design Automation Conference (DAC). pp. 637–642 (2021). https://doi.org/10.1109/DAC18074.2021.9586214

  29. [29]

    ACM Trans

    Hong, X., Zhou, X., Li, S., Feng, Y., Ying, M.: A Tensor Network based Decision Di- agram for Representation of Quantum Circuits. ACM Trans. Des. Autom. Electron. Syst.27(6), 60:1–60:30 (2022). https://doi.org/10.1145/3514355

  30. [30]

    In: Proceedings of the 53rd International Conference on Parallel Processing

    Jiang, S., Fu, R., Burgholzer, L., Wille, R., Ho, T.Y., Huang, T.W.: FlatDD: A High-Performance Quantum Circuit Simulator using Decision Diagram and Flat Array. In: Proceedings of the 53rd International Conference on Parallel Processing. pp. 388–399. ICPP ’24, Association for Computing Machinery, New York, NY, USA (2024). https://doi.org/10.1145/3673038.3673073

  31. [31]

    AddisonWesley Professional, Upper Saddle River, NJ, 1 edition edn

    Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 1 (Bitwise Tricks & Techniques; Binary Decision Diagrams). AddisonWesley Professional, Upper Saddle River, NJ, 1 edition edn. (2009)

  32. [32]

    Entropy26(12), 1058 (2024)

    Larsen, C.B., Olsen, S.B., Larsen, K.G., Schilling, C.: Contraction Heuristics for Tensor Decision Diagrams. Entropy26(12), 1058 (2024). https://doi.org/10.3390/ e26121058

  33. [33]

    IEEE Transactions on Parallel and Distributed Systems 31(4), 805–816 (2020)

    Li, R., Wu, B., Ying, M., Sun, X., Yang, G.: Quantum supremacy circuit simulation on sunway taihulight. IEEE Transactions on Parallel and Distributed Systems 31(4), 805–816 (2020). https://doi.org/10.1109/TPDS.2019.2947511

  34. [34]

    Lind-Nielsen, J.: Buddy : A binary decision diagram package. (1999)

  35. [35]

    IEEE Transactions on Computers60(10), 1377–1389 (2011)

    Lu, C.Y., Wang, S.A., Kuo, S.Y.: An Extended XQDD Representation for Multiple- Valued Quantum Logic. IEEE Transactions on Computers60(10), 1377–1389 (2011). https://doi.org/10.1109/TC.2011.114

  36. [36]

    SIAM Journal on Computing38(3), 963–981 (2008)

    Markov, I.L., Shi, Y.: Simulating Quantum Computation by Contracting Tensor Networks. SIAM Journal on Computing38(3), 963–981 (2008). https://doi.org/10. 1137/050644756

  37. [37]

    https://doi.org/10.48550/arXiv.2403.07197

    Mei, J., Bonsangue, M., Laarman, A.: Simulating Quantum Circuits by Model Counting (2024). https://doi.org/10.48550/arXiv.2403.07197

  38. [38]

    Springer New York, NY (2004)

    Molitor, P., Mohnke, J., Becker, B., Scholl, C.: Equivalence Checking of Digital Circuits: Fundamentals, Principles, Methods. Springer New York, NY (2004)

  39. [39]

    Journal of Physics A: Mathematical and Theoretical50(8), 084002 (2017)

    Montanaro, A.: Quantum circuits and low-degree polynomials over F2. Journal of Physics A: Mathematical and Theoretical50(8), 084002 (2017). https://doi.org/10. 1088/1751-8121/aa565f

  40. [40]

    npj Quantum Information 4(1), 1–12 (2018)

    Nam, Y., Ross, N.J., Su, Y., Childs, A.M., Maslov, D.: Automated optimization of large quantum circuits with continuous parameters. npj Quantum Information 4(1), 1–12 (2018). https://doi.org/10.1038/s41534-018-0072-4

  41. [41]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems35(1), 86–99 (2016)

    Niemann, P., Wille, R., Miller, D.M., Thornton, M.A., Drechsler, R.: QMDDs: Efficient Quantum Function Representation and Manipulation. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems35(1), 86–99 (2016). https://doi.org/10.1109/tcad.2015.2459034

  42. [42]

    Physical Review Letters128(3), 030501 (2022)

    Pan, F., Zhang, P.: Simulation of Quantum Circuits Using the Big-Batch Tensor Network Method. Physical Review Letters128(3), 030501 (2022). https://doi.org/ 10.1103/PhysRevLett.128.030501

  43. [43]

    IEEE Journal on Emerging and Selected Topics in Circuits and Systems12(3), 662–675 (2022)

    Peham, T., Burgholzer, L., Wille, R.: Equivalence Checking of Quantum Circuits With the ZX-Calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems12(3), 662–675 (2022). https://doi.org/10.1109/JETCAS.2022.3202204

  44. [44]

    arXiv:1403.2975 [quant-ph] (2016)

    Ross,N.J.,Selinger,P.:Optimalancilla-freeClifford+Tapproximationofz-rotations. arXiv:1403.2975 [quant-ph] (2016)

  45. [45]

    In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD)

    Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of 1993 International Conference on Computer Aided Design (ICCAD). pp. 42–47 (1993). https://doi.org/10.1109/ICCAD.1993.580029

  46. [46]

    In: Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III

    Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Computer Aided Verification: 35th International Conference, CAV 2023, Paris, France, July 17–22, 2023, Proceedings, Part III. pp. 213–225. Springer-Verlag, Berlin, Heidelberg (2023). https://doi.org/10.1007/978-3-031-37709-9_11

  47. [47]

    Weighted CFLOBDDs8(OOPSLA2), 320:1390–320:1419 (2024)

    Sistla, M., Chaudhuri, S., Reps, T.: Weighted Context-Free-Language Ordered Binary Decision Diagrams. Weighted CFLOBDDs8(OOPSLA2), 320:1390–320:1419 (2024). https://doi.org/10.1145/3689760

  48. [48]

    arXiv:2104.12101 [cs] (2021)

    Sølvsten, S.C., van de Pol, J., Jakobsen, A.B., Thomasen, M.W.B.: Efficient Binary Decision Diagram Manipulation in External Memory. arXiv:2104.12101 [cs] (2021)

  49. [49]

    University of Colorado at Boulder (2005)

    Somenzi, F.: CUDD: CU decision diagram package (release 3.0.0). University of Colorado at Boulder (2005)

  50. [50]

    In: 2021 58th ACM/IEEE Design Automa- tion Conference (DAC)

    Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-Slicing the Hilbert Space: Scaling Up Accurate Quantum Circuit Simulation. In: 2021 58th ACM/IEEE Design Automa- tion Conference (DAC). pp. 439–444 (2021). https://doi.org/10.1109/DAC18074. 2021.9586191

  51. [51]

    Quantum Information Processing2(5), 347–380 (2003)

    Viamontes, G.F., Markov, I.L., Hayes, J.P.: Improving Gate-Level Simulation of Quantum Circuits. Quantum Information Processing2(5), 347–380 (2003). https://doi.org/10.1023/b:qinp.0000022725.70000.4a

  52. [52]

    In: 2007 IEEE/ACM International Conference on Computer- Aided Design

    Viamontes, G.F., Markov, I.L., Hayes, J.P.: Checking equivalence of quantum circuits and states. In: 2007 IEEE/ACM International Conference on Computer- Aided Design. pp. 69–74. IEEE, San Jose, CA, USA (2007). https://doi.org/10. 1109/iccad.2007.4397246

  53. [53]

    Vilmart, R.: The structure of sum-over-paths, its consequences, and completeness for clifford (2020)

  54. [54]

    Vilmart, R.: Completeness of sum-over-paths for toffoli-hadamard and the dyadic fragments of quantum computation (2022)

  55. [55]

    Logical Methods in Computer ScienceV olume 20, Issue 1 (2024)

    Vilmart, R.: Rewriting and completeness of sum-over-paths in dyadic fragments of quantum computing. Logical Methods in Computer ScienceV olume 20, Issue 1 (2024). https://doi.org/10.46298/lmcs-20(1:20)2024

  56. [56]

    In: Caltais, G., Schilling, C

    Vinkhuijzen, L., Grurl, T., Hillmich, S., Brand, S., Wille, R., Laarman, A.: Efficient Implementation of LIMDDs for Quantum Circuit Simulation. In: Caltais, G., Schilling, C. (eds.) Model Checking Software. pp. 3–21. Springer Nature Switzerland, Cham (2023). https://doi.org/10.1007/978-3-031-32157-3_1

  57. [57]

    In: Meyers, R.A

    Watrous, J.: Quantum Computational Complexity. In: Meyers, R.A. (ed.) Encyclo- pedia of Complexity and Systems Science, pp. 7174–7201. Springer, New York, NY (2009). https://doi.org/10.1007/978-0-387-30440-3_428

  58. [58]

    SIAM monographs on discrete mathematics and applications, Society for Industrial and Applied Mathematics, Philadelphia (2000)

    Wegener, I.: Branching programs and binary decision diagrams: theory and appli- cations. SIAM monographs on discrete mathematics and applications, Society for Industrial and Applied Mathematics, Philadelphia (2000)

  59. [59]

    arXiv:2012.13966 [quant-ph] (2020)

    van de Wetering, J.: ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] (2020)

  60. [60]

    In: Int’l Symp

    Wille, R., Große, D., Teuber, L., Dueck, G.W., Drechsler, R.: RevLib: An online resource for reversible functions and reversible circuits. In: Int’l Symp. on Multi- Valued Logic. pp. 220–225 (2008)

  61. [61]

    ACM Transactions on Quantum Computing3(3), 13:1–13:17 (2022)

    Wille, R., Hillmich, S., Burgholzer, L.: Tools for Quantum Computing Based on Decision Diagrams. ACM Transactions on Quantum Computing3(3), 13:1–13:17 (2022). https://doi.org/10.1145/3491246

  62. [62]

    How to Efficiently Handle Complex Values? Implementing Decision Diagrams for Quantum Computing

    Zulehner, A., Hillmich, S., Wille, R.: How to Efficiently Handle Complex Values? Implementing Decision Diagrams for Quantum Computing. arXiv:1911.12691 [quant- ph] (2019)

  63. [63]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems38(5), 848–859 (2019)

    Zulehner, A., Wille, R.: Advanced Simulation of Quantum Computations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems38(5), 848–859 (2019). https://doi.org/10.1109/tcad.2018.2834427

This paper was first reviewed by deepseek-v4-flash on August 4, 2026.