Pith. sign in

REVIEW 4 major objections 5 minor 40 references

Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing

T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash

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

Pith's one-line read Q-Sylvan shows that edge-valued decision diagrams for quantum circuits can be parallelized, reporting an 18x speedup on 64 cores while staying competitive with a leading simulator on large instances.

desk verdict Useful parallel simulation package; equivalence checking not yet trustworthy. read the letter →

arxiv 2508.00514 v1 pith:V3FUSG6U submitted 2025-08-01 quant-ph

Sebastiaan Brand , Alfons Laarman This is my paper · ORCID
classification quant-ph MSC 68Q1268W1068P05 PACS 03.67.-a03.67.Lx
keywords quantumcircuitsimulationequivalencecheckingedge-valueddecisiondiagramsparallelalgorithmsworkstealinglock-freehashtableQ-Sylvan
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

The paper sets out to show that edge-valued decision diagrams (EVDDs), a compact data structure for quantum state vectors and matrices, can be efficiently parallelized for quantum tasks, something earlier attempts managed only poorly. It introduces Q-Sylvan, which combines fine-grained task parallelism from the Sylvan and Lace libraries with lock-free hash tables for complex edge values, and ships two use cases: circuit simulation and equivalence checking. The core reported result is a speedup of up to 18x on 64 cores on circuits whose diagrams have moderate sharing, together with single-core performance that is competitive with the MQT DDSIM simulator on large instances. If the claim holds, it means quantum circuit verification tools can ride multi-core hardware without giving up the compression that makes decision diagrams useful.

What carries the argument

The load-bearing object is the edge-valued decision diagram (EVDD), a rooted DAG whose edges carry complex numbers and whose paths multiply to vector entries or matrix elements; Q-Sylvan extends the Sylvan decision-diagram library with complex edge values. Three mechanisms carry the argument: a lock-free hash table that recognizes 'equivalent' complex values by rounding to a tolerance of delta = $10^{-14}$ and comparing components, which lets the DAG stay compact despite floating-point noise; norm-max normalization, which canonicalizes nodes by dividing child edge values by the larger child and multiplying the parent edge accordingly; and Lace-based fine-grained task parallelism, which spawns recursive calls in vector addition and matrix-vector multiplication as work-stealing tasks so many cores cooperate inside a single operation.

What would settle it

Run Q-Sylvan's equivalence checker on two circuits whose unitary matrices differ entrywise by a value below $10^{-14}$; if it reports them equivalent, the delta-merging has produced a false positive. Alternatively, compare Q-Sylvan's simulated state vector to a high-precision (rational or multi-precision) reference on a 30-qubit benchmark and look for amplitude errors exceeding the tool's own acceptance threshold.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is that EVDDs with complex edge values are not inherently hard to parallelize for quantum workloads: using work-stealing tasks and a lock-free hash table that stores rounded-then-compared floating-point edge values, Q-Sylvan achieves speedups up to 18x on 64 cores while remaining competitive with MQT DDSIM on a single core for larger circuits. The same machinery is applied to quantum circuit equivalence checking through two algorithms, the 'alternating' method and a Pauli-based method, the latter being the first decision-diagram implementation of that algorithm. The paper reports 8-core speedups of up to 5.8x on equivalence checking benchmarks and solves some instances faster than the portfolio tool MQT QCEC, while not matching its overall single-core throughput.

Load-bearing premise

The load-bearing premise is that treating complex edge values as equal when they differ by less than $10^{-14}$ never changes the answer: the paper relies on this tolerance for both simulation and equivalence checking, yet validates it mainly by checking $\ell^2$-norm near 1 and matching another simulator's outputs on circuits up to 20 qubits.

Editorial extensions

If this is right

  • On circuits whose decision diagrams have moderate sharing, Q-Sylvan's x18 speedup on 64 cores means quantum simulation and verification can use large multicore machines without abandoning DD compression.
  • The first DD-based Pauli equivalence-checking algorithm opens a practical route to verifying Clifford-heavy circuits inside a decision-diagram framework.
  • Because the same lock-free, delta-tolerant edge table serves both simulation and equivalence checking, any fix to numerical soundness would benefit both use cases.
  • If single-core performance on large instances is indeed competitive with MQT DDSIM, Q-Sylvan becomes a natural baseline for future quantum DD simulators.

Reading between the lines

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

  • Extending beyond the paper: the delta = 10^-14 merging is the part most likely to bite, since equivalence checking is a yes/no verdict and a false equivalence is silent; the paper's 'x' entries on VQE 5 suggest the risk is real, not hypothetical.
  • Extending beyond the paper: the speedups should carry over to stabilizer-like circuits, since the Pauli algorithm's polynomial behavior on Clifford gates gives the DD a very flat structure, though the paper does not test that directly.
  • Extending beyond the paper: the same parallel EVDD core could serve other linear-algebra workloads, such as tensor-network contraction, where the same multiplication and addition primitives appear.
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

4 major / 5 minor

Summary. The paper presents Q-Sylvan, a parallel edge-valued decision diagram (EVDD) package built on top of the Sylvan decision diagram library. The main technical contributions are an EVDD implementation with fine-grained task parallelism via work stealing and lock-free hash tables, including approximate floating-point edge-value merging and four normalization strategies, plus two use cases: quantum circuit simulation and equivalence checking. The empirical evaluation compares Q-Sylvan against MQT DDSIM, Quokka-Sharp, and MQT QCEC on MQT Bench and KetGPT circuits, reporting single-core performance competitive with DDSIM on large instances and parallel speedups up to 7.2x on 8 cores and 18x on 64 cores for a selected 'some sharing' category. The paper also reports equivalence-checking speedups up to 5.8x on 8 cores, but with lower completion rates than QCEC and with several 'x' entries indicating incorrect results.

Significance. If the parallelization approach is sound, the paper addresses a known obstacle: prior EVDD implementations for quantum workloads achieved only limited parallel speedups. The open-source release, reproducible benchmark scripts, and detailed per-instance tables are clear strengths, as is the systematic comparison against state-of-the-art tools. However, the correctness of the approximate floating-point merging is not established for equivalence checking, and the reported incorrect results in Tables 3 and 5 directly affect one of the two headline use cases. The simulation speedup claims are plausible, but the unqualified presentation of the 18x speedup and the 'competitive' single-core claim needs qualification. Overall the paper is a useful systems contribution, but the verification use case requires either a fix, an explicit limitation discussion, or a narrower claim.

major comments (4)
  1. [Section 5.2, Tables 3 and 5] The equivalence-checking results contain explicit 'x' entries indicating incorrect results: Q-Sylvan Pauli fails on Grover (no ancilla) 5, Grover (v-chain) 5, and Q-walk (v-chain) 5, and both Q-Sylvan alternating and Pauli fail on VQE 5, among others. The text reports the completion percentages and speedups but never discusses these incorrect answers. Since equivalence checking is one of the two main use cases advertised in the abstract and introduction, the paper must either fix the underlying bug, explain the conditions under which such failures occur, or explicitly restrict the equivalence-checking claims to the instances that were verified correct.
  2. [Section 3, Algorithm 3 and 'Floating-point equality'] The approximate equality relation |a-b| < δ with δ=10^-14 is not transitive, and the chosen norm-max normalization folds approximation into edge values. The validation in Section 5.1 only checks that simulated state vectors have l2-norm near 1 and matches DDSIM outputs up to 20 qubits; it does not validate equivalence-checking outputs against ground truth. The 'x' entries in Tables 3 and 5 are a direct symptom of this gap. The paper needs a correctness argument or an experimental validation of equivalence checking on small circuits against explicit unitary matrices, or a sensitivity analysis showing that the chosen δ does not change answers on the reported benchmarks.
  3. [Section 5.1, Figure 4a and abstract] The headline 'parallel speedups of up to x18 on 64 cores' is the P99 of the KetGPT 'some sharing' category, while the same table reports 64-core speedups as low as x0.5-x0.7 for the high-sharing category (i.e., slowdowns). The abstract and introduction present the x18 figure without this context. Please qualify the claim to the specific sharing category and percentile, or explain why the slowdowns on high-sharing diagrams do not affect the stated use cases.
  4. [Section 5.1, Figure 3] The claim that Q-Sylvan is 'competitive with MQT DDSIM on large instances' is based on a post-hoc subset: circuits where either tool takes at least 10 seconds. This selection criterion should be stated as the formal definition of 'large instances,' and the number of circuits in that subset should be reported alongside the 61% and 30% win rates. Additionally, all reported runtimes appear to be from single runs with no variance or repeated measurements; for speedup claims, at least median or geomean over several runs is expected.
minor comments (5)
  1. [Section 3] The text 'δ = 10914' before Algorithm 3 appears to be a typo; the intended value is 10^-14 as stated in the algorithm caption and elsewhere.
  2. [Figure 2 caption] The definition of norm-L2 is terse: please specify the phase θ and explain why normalizing by α/ν ∈ R+ is always achievable, or cite a reference for this normalization.
  3. [Section 5.1] The sentence 'we verified the full state vector output of both tools up to 20 qubits' should report the number of circuits checked and the numerical tolerance used for the comparison.
  4. [Table 1] The term 'runtime reduction' is not defined; please state whether it is the ratio of total runtimes on solved instances, a per-instance geometric mean, or some other aggregate.
  5. [Figures 3 and 4] The open markers for timeouts are defined in the text and captions, but some subfigures lack an explicit legend; adding one would improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claims are benchmark measurements against external tools, not derivations that reduce to fitted inputs or self-citations.

full rationale

The paper's central claims are empirical performance results: parallel speedups up to ×18 on 64 cores and single-core competitiveness with MQT DDSIM on large instances. These are measured against external tools and benchmark suites (MQT Bench, KetGPT, MQT QCEC, Quokka-Sharp), so they do not reduce by construction to any fitted parameter or to the paper's own assumptions. The δ=10^-14 floating-point tolerance and norm-max normalization are engineering choices, transparently described as tuned before the Section 5 evaluation, but they are not presented as predictions nor used to force the measured comparison; the benchmarks are direct experiments. Citations to Sylvan, Lace, and the Pauli theorem [33, Thm.1] are either implementation-building-block citations or a parameter-free mathematical theorem, so they constitute independent support rather than a load-bearing self-citation chain. The '×' entries in Tables 3/5 indicate incorrect equivalence-checking results, but that is a correctness/robustness concern about approximate floating-point merging, not circularity: the performance claims do not become equivalent to their inputs because of it.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The paper's central claims rest on the standard correctness of EVDD operations, the cited Pauli criterion, and the authors' choice of a floating-point tolerance and normalization strategy. No new physical or mathematical entities are introduced.

free parameters (2)
  • delta (floating-point equality tolerance) = 10^-14
    Hand-set threshold for considering two complex edge values equivalent; controls node merging and can affect the correctness of simulation and equivalence checking.
  • normalization strategy = norm-max
    Chosen as default after benchmarking four strategies on MQT Bench; affects canonicity and numerical stability, and was selected by performance rather than derived.
assumptions (3)
  • domain assumption Pauli equivalence criterion: U is equivalent to V iff for all j, U X_j U-dagger equals V X_j V-dagger and U Z_j U-dagger equals V Z_j V-dagger.
    Invoked in Section 4 Pauli algorithm, cited to [33, Thm.1]; Q-Sylvan relies on this theorem being correct for the gate sets used.
  • ad hoc to paper Approximate floating-point equality with delta=10^-14 is a valid equivalence relation for EVDD edge values.
    Section 3 and Algorithm 3; not proved, and the VQE 5 incorrect results in Tables 3 and 5 suggest it can fail in equivalence checking.
  • standard math Standard EVDD semantics: path products equal vector or matrix entries, and recursive Plus and Multiply algorithms implement vector addition and matrix-vector multiplication.
    Assumed from the DD literature [11,31,23], used in Algorithms 1 and 2.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing." pith.science (2026). https://pith.science/paper/V3FUSG6U

@misc{pith2026250800514,
  author       = {Pith},
  title        = {Pith review of: Q-Sylvan: A Parallel Decision Diagram Package for Quantum Computing},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/V3FUSG6U}},
  note         = {Machine review of arXiv:2508.00514}
}
read the original abstract

As physical realizations of quantum computers move closer towards practical applications, the need for tools to analyze and verify quantum algorithms grows. Among the algorithms and data structures used to tackle such problems, decision diagrams (DDs) have shown much success. However, an obstacle with DDs is their efficient parallelization, and while parallel speedups have been obtained for DDs used in classical applications, attempts to parallelize operations for quantum-specific DDs have yielded only limited success. In this work, we present an efficient implementation of parallel edge-valued DDs, which makes use of fine-grained task parallelism and lock-free hash tables. Additionally, we use these DDs to implement two use cases: simulation and equivalence checking of quantum circuits. In our empirical evaluation we find that our tool, Q-Sylvan, shows a single-core performance that is competitive with the state-of-the-art quantum DD tool MQT DDSIM on large instances, and moreover achieves parallel speedups of up to x18 on 64 cores.

Figures

Figures reproduced from arXiv: 2508.00514 by the authors.

Figure 1
Figure 1. A 2 n ×2 n matrix (a) can be recursively encoded in a DD with two children per node (b), as in EVDD [31], or four children per node (c), as in QMDD [23]. x0 x1 x2 x2 ⊤ 3 92 i An EVDD is a rooted, directed, acyclic graph whose edges have values associated with them. For our purposes these values are complex numbers. Each node v in an EVDD has a variable var(v) = xi , and two outgoing edges. For an EVDD that encodes a… view at source ↗
Figure 2
Figure 2. An arbitrary tuple of edge values ⟨α, β, γ⟩ is not generally in a canonical form, e.g. ⟨2, 6, 1⟩ ≡ ⟨1, 3, 2⟩. Such a tuple can be normalized by dividing α and β, and multiplying γ, by some choice of ν. In the example, normalizing both tuples by ν = α yields ⟨ 2 2 , 6 2 , 1 · 2⟩ = ⟨1, 3, 2⟩ and ⟨ 1 1 , 3 1 , 2 · 1⟩ = ⟨1, 3, 2⟩. The table in (c) shows different choices for ν, along with an empirical evaluation of the … view at source ↗
Figure 3
Figure 3. Q-Sylvan vs DDSIM. Both order variables according to the qubit ordering in the QASM file. Open markers indicate timeouts. For both plots, we verified the full state vector output of both tools up to 20 qubits. While DDSIM is faster on the smaller circuits, on circuits where either tool takes ≥ 10 seconds Q-Sylvan beats DDSIM in 61% of MQT Bench circuits, and 30% of KetGPT circuits. circuits, we evaluate Q-Sylvan’s m… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Parallel performance. Open markers indicate timeouts, dashed lines indicate equal performance, and dotted lines indicate a ×k speedup for k-cores [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 36 canonical work pages

  1. [1]

    In: Proceedings of the forty- second ACM symposium on Theory of computing

    Aaronson, S.: BQP and the polynomial hierarchy. In: Proceedings of the forty- second ACM symposium on Theory of computing. pp. 141–150 (2010)

    work page 2010

  2. [2]

    In: International Conference on Computa- tional Science

    Apak, B., Bandic, M., Sarkar, A., Feld, S.: KetGPT–Dataset augmentation of quantum circuits using transformers. In: International Conference on Computa- tional Science. pp. 235–251. Springer (2024)

    work page 2024

  3. [3]

    IEEE Transactions on TCAD40(9), 1810–1824 (2020)

    Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Transactions on TCAD40(9), 1810–1824 (2020)

    work page 2020

  4. [4]

    Chemical reviews119(19), 10856–10915 (2019)

    Cao, Y., Romero, J., Olson, J.P., Degroote, M., Johnson, P.D., Kieferová, M., Kivlichan, I.D., Menke, T., Peropadre, B., Sawaya, N.P., et al.: Quantum chemistry in the age of quantum computing. Chemical reviews119(19), 10856–10915 (2019)

    work page 2019

  5. [5]

    arXiv preprint arXiv:1707.03429 (2017)

    Cross, A.W., Bishop, L.S., Smolin, J.A., Gambetta, J.M.: Open quantum assembly language. arXiv preprint arXiv:1707.03429 (2017)

    arXiv 2017

  6. [6]

    Dawson,C.M.,Nielsen,M.A.:TheSolovay-Kitaevalgorithm.arXivpreprintquant- ph/0505030 (2005)

    arXiv 2005

  7. [7]

    Electronic Notes in Theoretical Computer Science 296, 127–143 (2013)

    van Dijk, T., Laarman, A., Van De Pol, J.: Multi-core BDD operations for symbolic reachability. Electronic Notes in Theoretical Computer Science 296, 127–143 (2013)

    work page 2013

  8. [8]

    STTT 19, 675–696 (2017)

    van Dijk, T., Van de Pol, J.: Sylvan: multi-core framework for decision diagrams. STTT 19, 675–696 (2017)

    work page 2017

Show all 40 references
  1. [9]

    In: Euro-Par 2014: Parallel Processing Workshops: Euro-Par 2014 International Workshops, Porto, Portugal, August 25-26, 2014, Revised Selected Papers, Part II

    van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Euro-Par 2014: Parallel Processing Workshops: Euro-Par 2014 International Workshops, Porto, Portugal, August 25-26, 2014, Revised Selected Papers, Part II

    2014

  2. [10]

    Proceedings of the AAAI Conference on Artificial Intelligence 28(1) (2014)

    Fargier, H., Marquis, P., Niveau, A., Schmidt, N.: A knowledge compilation map for ordered real-valued decision diagrams. Proceedings of the AAAI Conference on Artificial Intelligence 28(1) (2014)

    2014

  3. [11]

    Formal methods in system design 10, 149–169 (1997)

    Fujita, M., McGeer, P.C., Yang, J.Y.: Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal methods in system design 10, 149–169 (1997)

    1997

  4. [12]

    IEEE Transactions on Quantum Engineering2, 1–17 (2021)

    Harwood, S., Gambella, C., Trenev, D., Simonetto, A., Bernal, D., Greenberg, D.: Formulating and solving routing problems on quantum computers. IEEE Transactions on Quantum Engineering2, 1–17 (2021)

    2021

  5. [13]

    In: 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC)

    Hillmich, S., Zulehner, A., Wille, R.: Concurrency in DD-based quantum circuit simulation. In: 2020 25th Asia and South Pacific Design Automation Conference (ASP-DAC). pp. 115–120. IEEE (2020)

    2020

  6. [14]

    arXiv preprint arXiv:2504.01168 (2025)

    Hong, X., Dai, A., Gao, D., Li, S., Ji, Z., Ying, M.: LimTDD: A compact decision diagram integrating tensor and local invertible map representations. arXiv preprint arXiv:2504.01168 (2025)

    2025

  7. [15]

    Science377(6613) (2022)

    Huang, H.Y., Kueng, R., Torlai, G., Albert, V.V., Preskill, J.: Provably efficient machine learning for quantum many-body problems. Science377(6613) (2022)

    2022

  8. [16]

    Non-identity-check

    Janzing, D., Wocjan, P., Beth, T.: "Non-identity-check" is QMA-complete. Inter- national Journal of Quantum Information3(03), 463–473 (2005)

    2005

  9. [17]

    arXiv preprint arXiv:0906.5416 (2009)

    Ji, Z., Wu, X.: Non-identity check remains QMA-complete for short circuits. arXiv preprint arXiv:0906.5416 (2009)

    2009 arXiv

  10. [18]

    Russian Mathematical Surveys 52(6), 1191 (1997)

    Kitaev, A.Y.: Quantum computations: algorithms and error correction. Russian Mathematical Surveys 52(6), 1191 (1997)

    1997

  11. [19]

    In: Formal Methods in Computer Aided Design

    Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability perfor- mance with shared hash tables. In: Formal Methods in Computer Aided Design. pp. 247–255. IEEE (2010) 13

    2010

  12. [20]

    pp. 206–217. Springer (2014)

    2014

  13. [21]

    IEEE Transactions on Quantum Engineering (2024)

    Li, S., Kimura, Y., Sato, H., Fujita, M.: Parallelizing quantum simulation with decision diagrams. IEEE Transactions on Quantum Engineering (2024)

    2024

  14. [22]

    In: Proceedings of the 30th international design automation conference

    Matsunaga, Y., McGeer, P.C., Brayton, R.K.: On computing the transitive closure of a state transition relation. In: Proceedings of the 30th international design automation conference. pp. 260–265 (1993)

    1993

  15. [23]

    In: International Joint Conference on Automated Reasoning

    Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. In: International Joint Conference on Automated Reasoning. pp. 401–421. Springer (2024)

    2024

  16. [24]

    In: 36th International Symposium on Multiple-Valued Logic (ISMVL’06)

    Miller, D.M., Thornton, M.A.: QMDD: A decision diagram structure for reversible and quantum circuits. In: 36th International Symposium on Multiple-Valued Logic (ISMVL’06). pp. 30–30. IEEE (2006)

    2006

  17. [25]

    IEEE TCAD 39(12), 4657–4668 (2020)

    Niemann, P., Zulehner, A., Drechsler, R., Wille, R.: Overcoming the tradeoff between accuracy and compactness in decision diagrams for quantum computation. IEEE TCAD 39(12), 4657–4668 (2020)

    2020

  18. [26]

    Reviews in Physics4, 100028 (2019)

    Orús, R., Mugel, S., Lizaso, E.: Quantum computing for finance: Overview and prospects. Reviews in Physics4, 100028 (2019)

    2019

  19. [27]

    Quantum (2023), MQT Bench is available at https://www.cda.cit.tum.de/mqtbench/

    Quetschlich, N., Burgholzer, L., Wille, R.: MQT Bench: Benchmarking software and design automation tools for quantum computing. Quantum (2023), MQT Bench is available at https://www.cda.cit.tum.de/mqtbench/

    2023

  20. [28]

    In: European Symposium on Algorithms

    Samoladas, V.: Improved BDD algorithms for the simulation of quantum circuits. In: European Symposium on Algorithms. pp. 720–731. Springer (2008)

    2008

  21. [29]

    arXiv preprint arXiv:1212.6253 (2012)

    Selinger, P.: Efficient Clifford+T approximation of single-qubit operators. arXiv preprint arXiv:1212.6253 (2012)

    2012 arXiv

  22. [30]

    In: FOCS

    Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factor- ing. In: FOCS. pp. 124–134. IEEE (1994)

    1994

  23. [31]

    Sistla,M.,Chaudhuri,S.,Reps,T.:SymbolicquantumsimulationwithQuasimodo. In: CAV. pp. 213–225. Springer (2023)

    2023

  24. [32]

    Formal Methods in System Design10, 243–270 (1997)

    Tafertshofer, P., Pedram, M.: Factored edge-valued binary decision diagrams. Formal Methods in System Design10, 243–270 (1997)

    1997

  25. [33]

    International Journal of Quantum Information 8(05), 807–819 (2010)

    Tanaka, Y.: Exact non-identity check is NQP-complete. International Journal of Quantum Information 8(05), 807–819 (2010)

    2010

  26. [34]

    In: International Symposium on Automated Technology for Verification and Analysis

    Thanos, D., Coopmans, T., Laarman, A.: Fast equivalence checking of quantum circuits of Clifford gates. In: International Symposium on Automated Technology for Verification and Analysis. pp. 199–216. Springer (2023)

    2023

  27. [35]

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

    Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-slicing the Hilbert space: Scaling up ac- curate quantum circuit simulation. In: 2021 58th ACM/IEEE Design Automation Conference (DAC). pp. 439–444. IEEE (2021)

    2021

  28. [36]

    In: Proceedings Design, Automation and Test in Europe Conference and Exhibition

    Viamontes, G.F., Markov, I.L., Hayes, J.P.: High-performance QuIDD-based simulation of quantum circuits. In: Proceedings Design, Automation and Test in Europe Conference and Exhibition. vol. 2, pp. 1354–1355. IEEE (2004)

    2004

  29. [37]

    Quantum 7, 1108 (2023)

    Vinkhuijzen, L., Coopmans, T., Elkouss, D., Dunjko, V., Laarman, A.: LIMDD: A decision diagram for simulation of quantum computing including stabilizer states. Quantum 7, 1108 (2023)

    2023

  30. [38]

    In: International Symposium on Model Checking Software

    Vinkhuijzen, L., Grurl, T., Hillmich, S., Brand, S., Wille, R., Laarman, A.: Efficient implementation of LIMDDs for quantum circuit simulation. In: International Symposium on Model Checking Software. pp. 3–21. Springer (2023)

    2023

  31. [39]

    In: Proceedings of the 59th Design Automation Conference

    Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate BDD-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th Design Automation Conference. pp. 523–528 (2022)

    2022

  32. [40]

    -” indicates an out-of- memory termination, and “×

    Zulehner, A., Wille, R.: Advanced simulation of quantum computations. IEEE TCAD 38(5), 848–859 (2018) 14 S. Brand and A. Laarman A Additional results T able 2.Simulation times on a subset of MQT Bench circuits. Algorithm n Q-Sylvan (EVDD) MQT DDSIM (EVDD) Quasimodo (CLFOBDD) A...

    2018

Pith tools

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