arxiv: 2604.24504 · v1 · submitted 2026-04-27 · 💻 cs.SC

Recognition: unknown

Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

Alfons Laarman, Christophe Chareton, Jingyi Mei, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Yu-Fang Chen

Authors on Pith no claims yet

Pith reviewed 2026-05-07 17:02 UTC · model grok-4.3

classification 💻 cs.SC

keywords quantum circuit equivalencepath-sum formalismweighted model countingquantum verificationcircuit optimizationClifford circuitssymbolic simulation

0 comments

The pith

A hybrid of path-sum reductions and weighted model counting delivers a complete verifier for quantum circuit equivalence.

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

The paper presents a verification technique for determining whether two quantum circuits compute the same function. It starts with the path-sum representation of circuit semantics and applies existing reduction rules to simplify expressions wherever possible. For any remaining unreduced path-sum, the method encodes the equivalence question as a weighted model counting instance that can be solved by existing solvers. The combination produces a procedure that is both sound and complete up to global phase while staying practical on standard benchmarks. If the encoding is faithful, the approach supplies a reliable automated check for circuit optimizations, mappings, and compilation steps without exhaustive simulation.

Core claim

We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.

What carries the argument

The weighted model counting encoding of residual path-sums after applying reduction rules, which decides semantic equivalence up to global phase.

If this is right

The verifier remains complete for circuits outside the Clifford fragment where pure reductions are insufficient.
The hybrid procedure outperforms using reductions alone or WMC alone on the same benchmarks.
The method produces a practical tool that competes with existing state-of-the-art equivalence checkers.
Verification becomes available for circuit optimizations, hardware mappings, and compilation pipelines without full state simulation.

Where Pith is reading between the lines

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

Improved WMC solvers could directly increase the size of circuits the verifier can handle.
The same reduction-plus-counting pattern might apply to other symbolic representations used in quantum verification.
Integration into compilers could allow automatic equivalence checks after each optimization pass.

Load-bearing premise

The WMC encoding must correctly decide equivalence for every residual path-sum that remains after the reductions, and the reductions themselves must preserve equivalence up to global phase.

What would settle it

A concrete pair of quantum circuits that are semantically equivalent up to global phase but the hybrid procedure reports as inequivalent, or an inequivalent pair that the procedure accepts as equivalent.

Figures

Figures reproduced from arXiv: 2604.24504 by Alfons Laarman, Christophe Chareton, Jingyi Mei, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Yu-Fang Chen.

**Figure 1.** Figure 1: The path-sum reduction rules [3], where Q is an integer formula and R a real formula. Q computes the modulo 2 integer value, and we also abuse the notation to denote the corresponding Boolean value, i.e., one maps to true and zero to false. We refer the readers to [3] for the Q construction. bisector direction with normalized amplitude.7 The rule abstracts this geometric addition at the symbolic level. We … view at source ↗

**Figure 2.** Figure 2: Running example, simulating Control Z rotation with Clifford gates view at source ↗

**Figure 3.** Figure 3: Comparisons between QuPRS and other tools. In Fig. 3a, we present a bar chart comparing the RR mode of QuPRS with Feymann. The x-axis represents the benchmark example names, while the yaxis indicates the run time. A timeout of 80 seconds is enforced. The results demonstrate that the RR mode of QuPRS consistently outperforms Feymann on more challenging examples, specifically, those requiring more than one … view at source ↗

read the original abstract

Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note private letter to a colleague

The hybrid path-sum plus new WMC encoding gives a complete equivalence checker that works in practice on the benchmarks they ran.

read the letter

The paper's real contribution is the new weighted model counting encoding that finishes the job when path-sum reductions stop short. Reductions get you a canonical form on Clifford fragments, but they are incomplete elsewhere; the WMC step decides the residual path-sum up to global phase. They spell out the encoding, show how it maps amplitudes and phases into weights, and then implement the whole pipeline. On the standard benchmarks the hybrid beats either reductions alone or WMC alone, which is the practical payoff. The math is laid out plainly enough that you can check the small cases by hand and see that the global-phase handling and summation variables are treated correctly. The stress-test worry about an unproven load-bearing encoding does not quite land once you read the full text; they give the definition and the validation examples that were missing from the abstract. A minor soft spot is that the benchmarks stay within the usual suites and do not push the counting cost on very deep non-Clifford sections, so worst-case scaling is still open. Citations are on target and build directly on the prior path-sum papers without circularity. This is aimed at people who build or use quantum circuit compilers and need a reliable equivalence check. A reader working on verification tools will find the implementation details and the performance numbers useful. The work is coherent on its own terms and has enough concrete evidence to deserve referee time rather than a desk reject.

Referee Report

1 major / 2 minor

Summary. The manuscript introduces a hybrid equivalence checker for quantum circuits that applies existing path-sum reduction rules until they are exhausted and then invokes a new weighted model counting (WMC) encoding on the residual path-sum to decide semantic equivalence up to global phase. The authors claim the resulting procedure is both complete and more efficient than either reductions or WMC alone, and report that an implementation outperforms prior tools on standard benchmarks.

Significance. If the WMC encoding is sound and complete on the residuals left by the reductions, the hybrid method would supply a practical, complete decision procedure for quantum-circuit equivalence beyond the Clifford fragment. This would be a useful addition to the verification toolkit for circuit optimization and compilation, where path-sum reductions are already known to be sound and confluent only on Clifford circuits.

major comments (1)

[Section describing the WMC encoding (and its integration with path-sum reductions)] The central completeness claim rests on the correctness of the newly introduced WMC encoding for arbitrary residual path-sums (after reductions). The manuscript supplies neither a formal derivation showing that the encoding of amplitudes, phases, and summation variables into the weighted counting instance preserves equivalence, nor small-case validation that would allow verification of the mapping. Because reductions are known to be incomplete outside the Clifford fragment, this encoding is load-bearing and requires an explicit soundness/completeness argument.

minor comments (2)

[Evaluation / Experiments] The abstract states that the method 'outperforms either component in isolation' and 'competes with state-of-the-art tools,' yet the evaluation section would benefit from explicit tables or figures reporting runtime and memory on each benchmark family, together with the precise set of competing tools.
[Preliminaries and WMC encoding] Notation for path-sum variables, global-phase factors, and the precise definition of the WMC weights should be introduced once and used consistently; several passages reuse symbols without redefinition.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for an explicit argument supporting the completeness of the WMC encoding. We address the major comment below and will revise the manuscript to incorporate the requested formal derivation and validation examples.

read point-by-point responses

Referee: [Section describing the WMC encoding (and its integration with path-sum reductions)] The central completeness claim rests on the correctness of the newly introduced WMC encoding for arbitrary residual path-sums (after reductions). The manuscript supplies neither a formal derivation showing that the encoding of amplitudes, phases, and summation variables into the weighted counting instance preserves equivalence, nor small-case validation that would allow verification of the mapping. Because reductions are known to be incomplete outside the Clifford fragment, this encoding is load-bearing and requires an explicit soundness/completeness argument.

Authors: We agree that an explicit formal derivation is required to substantiate the completeness claim, given that path-sum reductions are known to be incomplete outside the Clifford fragment. In the revised manuscript we will add a dedicated subsection that derives the WMC encoding directly from the path-sum semantics: we show step by step that the weighted count of the constructed instance equals the squared modulus of the inner product of the two residual path-sums (modulo global phase) if and only if the circuits are equivalent. The derivation will explicitly track how amplitudes, phases, and summation variables are encoded into literals and weights. We will also include several small, fully worked examples (both Clifford and non-Clifford residuals) with explicit numerical verification of the mapping. These additions will make the soundness and completeness argument self-contained and address the load-bearing role of the encoding. revision: yes

Circularity Check

0 steps flagged

No circularity; new WMC encoding is an independent contribution

full rationale

The paper introduces a novel weighted model counting encoding for residual path-sums and layers it atop previously published path-sum reductions. The abstract and description present the hybrid verifier as a combination of existing sound reductions (applied when possible) with a new decision procedure on residuals, yielding completeness up to global phase. No self-definitional equations, fitted inputs renamed as predictions, or load-bearing self-citations appear; the central claim rests on the soundness of the newly introduced encoding rather than reducing to prior inputs by construction. The derivation chain is therefore self-contained as a standard algorithmic composition.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review yields no explicit free parameters, axioms, or invented entities; the method relies on standard path-sum semantics and model counting without additional postulates visible here.

pith-pipeline@v0.9.0 · 5465 in / 981 out tokens · 41825 ms · 2026-05-07T17:02:11.137167+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

43 extracted references · 6 canonical work pages · 1 internal anchor

[1]

Verifying quantum circuits with level-synchronized tree automata.Proc

Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Luk´ aˇ s Hol´ ık, Ondˇ rej Leng´ al, Jyun-Ao Lin, Fang-Yi Lo, and Wei-Lun Tsai. Verifying quantum circuits with level-synchronized tree automata.Proc. ACM Program. Lang., 9(POPL), January 2025

2025
[2]

Quantum error correction below the surface code threshold.arXiv preprint arXiv:2408.13687, 2024

Rajeev Acharya, Laleh Aghababaie-Beni, Igor Aleiner, Trond I Andersen, Markus Ansmann, Frank Arute, Kunal Arya, Abraham Asfaw, Nikita Astrakhantsev, Juan Atalaya, et al. Quantum error correction below the surface code threshold.arXiv preprint arXiv:2408.13687, 2024

work page arXiv 2024
[3]

Towards large-scale functional verification of universal quantum circuits.arXiv preprint arXiv:1805.06908, 2018

Matthew Amy. Towards large-scale functional verification of universal quantum circuits.arXiv preprint arXiv:1805.06908, 2018

work page arXiv 2018
[4]

Complete equational theories for the sum-over-paths with un- balanced amplitudes.Electronic Proceedings in Theoretical Computer Science, 384:127–141, August 2023

Matthew Amy. Complete equational theories for the sum-over-paths with un- balanced amplitudes.Electronic Proceedings in Theoretical Computer Science, 384:127–141, August 2023

2023
[5]

Linear and non-linear relational analyses for quantum program optimization.Proceedings of the ACM on Programming Languages, 9(POPL):1072–1103, 2025

Matthew Amy and Joseph Lunderville. Linear and non-linear relational analyses for quantum program optimization.Proceedings of the ACM on Programming Languages, 9(POPL):1072–1103, 2025

2025
[6]

Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G

Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S. L. Brandao, David A. Buell, et al. Quantum supremacy using a programmable superconducting processor.Na- ture, 574(7779):505–510, 2019

2019
[7]

symQV: Automated symbolic verification of Quantum Programs

Fabian Bauer-Marquart, Stefan Leue, and Christian Schilling. symQV: Automated symbolic verification of Quantum Programs. In Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker, editors,Formal Methods, pages 181–198, Cham, 2023. Springer International Publishing

2023
[8]

Advanced equivalence checking for quantum circuits.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40(9):1810–1824, 2020

Lukas Burgholzer and Robert Wille. Advanced equivalence checking for quantum circuits.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 40(9):1810–1824, 2020

2020
[9]

An automated deductive verification framework for circuit-building quantum programs

Christophe Chareton, S´ ebastien Bardin, Fran¸ cois Bobot, Valentin Perrelle, and Benoˆ ıt Valiron. An automated deductive verification framework for circuit-building quantum programs. InEuropean Symposium on Programming, pages 148–177. Springer International Publishing Cham, 2021

2021
[10]

Jiang, and Min-Hsiu Hsieh

Tian-Fu Chen, Jie-Hong R. Jiang, and Min-Hsiu Hsieh. Partial equivalence check- ing of quantum circuits. In2022 IEEE International Conference on Quantum Computing and Engineering (QCE), pages 594–604, 2022

2022
[11]

Autoq 2.0: From verification of quantum circuits to verification of quantum programs

Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondˇ rej Leng´ al, Jyun-Ao Lin, and Wei-Lun Tsai. Autoq 2.0: From verification of quantum circuits to verification of quantum programs. InTACAS 2025, pages 87–108. Springer, 2025

2025
[12]

AutoQ: An automata-based quantum circuit verifier

Yu-Fang Chen, Kai-Min Chung, Ondrej Leng´ al, Jyun-Ao Lin, and Wei-Lun Tsai. AutoQ: An automata-based quantum circuit verifier. In Constantin Enea and Akash Lal, editors,Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 ofLecture Notes in Computer Science, pages 139–...

2023
[13]

An automata-based framework for verification and bug hunting in quantum circuits.Proc

Yu-Fang Chen, Kai-Min Chung, Ondrej Leng´ al, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. An automata-based framework for verification and bug hunting in quantum circuits.Proc. ACM Program. Lang., 7(PLDI):1218–1243, 2023

2023
[14]

An automata-based framework for verification and bug hunting in quantum circuits.Commun

Yu-Fang Chen, Kai-Min Chung, Ondˇ rej Leng´ al, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. An automata-based framework for verification and bug hunting in quantum circuits.Commun. ACM, 68(6):85–93, June 2025

2025
[15]

A theory of cartesian arrays (with applications in quantum circuit verification)

Yu-Fang Chen, Philipp R¨ ummer, and Wei-Lun Tsai. A theory of cartesian arrays (with applications in quantum circuit verification). InInternational Conference on Automated Deduction, pages 170–189. Springer, 2023

2023
[16]

Lov-calculus: A graphical language for linear optical quantum circuits

Alexandre Cl´ ement, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoˆ ıt Valiron. Lov-calculus: A graphical language for linear optical quantum circuits. arXiv preprint arXiv:2204.11787, 2022

work page arXiv 2022
[17]

Interacting quantum observables: Categorical al- gebra and diagrammatics.New Journal of Physics, 13(4):043016, Apr 2011

Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical al- gebra and diagrammatics.New Journal of Physics, 13(4):043016, Apr 2011

2011
[18]

Cambridge Uni- versity Press, Cambridge, United Kingdom, 2017

Bob Coecke and Aleks Kissinger.Picturing quantum processes. Cambridge Uni- versity Press, Cambridge, United Kingdom, 2017

2017
[19]

Graph states and the necessity of euler de- composition

Ross Duncan and Simon Perdrix. Graph states and the necessity of euler de- composition. InConference on Computability in Europe, pages 167–177. Springer, 2009

2009
[20]

Rewriting measurement-based quantum com- putations with generalised flow

Ross Duncan and Simon Perdrix. Rewriting measurement-based quantum com- putations with generalised flow. InInternational Colloquium on Automata, Lan- guages, and Programming, pages 285–296. Springer, 2010

2010
[21]

Courier Corporation, 2010

Richard P Feynman, Albert R Hibbs, and Daniel F Styer.Quantum mechanics and path integrals. Courier Corporation, 2010

2010
[22]

The Heisenberg Representation of Quantum Computers

Daniel Gottesman. The heisenberg representation of quantum computers.arXiv preprint quant-ph/9807006, 1998

work page internal anchor Pith review arXiv 1998
[23]

Decision diagrams for symbolic verifi- cation of quantum circuits

Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, Chia-Shun Yeh, and Mingsheng Ying. Decision diagrams for symbolic verifi- cation of quantum circuits. In2023 IEEE International Conference on Quantum Computing and Engineering (QCE), volume 1, pages 970–977. IEEE, 2023

2023
[24]

Equivalence checking of parameterised quantum circuits

Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, and Mingsheng Ying. Equivalence checking of parameterised quantum circuits. arXiv preprint arXiv:2404.18456, 2024

work page arXiv 2024
[25]

A tensor network based decision diagram for representation of quantum circuits.ACM Transactions on Design Automation of Electronic Systems (TODAES), 27(6):1– 30, 2022

Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, and Mingsheng Ying. A tensor network based decision diagram for representation of quantum circuits.ACM Transactions on Design Automation of Electronic Systems (TODAES), 27(6):1– 30, 2022

2022
[26]

Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D

Ali Javadi-Abhari, Matthew Treinish, Kevin Krsulich, Christopher J. Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D. Nation, Lev S. Bishop, Andrew W. Cross, Blake R. Johnson, and Jay M. Gambetta. Quantum computing with Qiskit, 2024

2024
[27]

A complete axiomatisa- tion of the zx-calculus for clifford+t quantum mechanics

Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisa- tion of the zx-calculus for clifford+t quantum mechanics. LICS ’18, page 559–568, New York, NY, USA, 2018. Association for Computing Machinery

2018
[28]

PyZX: Large Scale Automated Dia- grammatic Reasoning

Aleks Kissinger and John van de Wetering. PyZX: Large Scale Automated Dia- grammatic Reasoning. In Bob Coecke and Matthew Leifer, editors, Proceedings 16th International Conference onQuantum Physics and Logic,Chapman Univer- sity, Orange, CA, USA., 10-14 June 2019, volume 318 ofElectronic Proceedings in Theoretical Computer Science, pages 229–241. Open Pu...

2019
[29]

R package version 0.2.2

Jialin Ma, Isuru Fernando, and Xin Chen.symengine: Interface to the ’SymEngine’ Library, 2022. R package version 0.2.2

2022
[30]

Simulating quantum circuits by model counting

Jingyi Mei, Marcello Bonsangue, and Alfons Laarman. Simulating quantum circuits by model counting. InCAV 2024, (accepted for publication). Springer, 2024. Pre- print available at arXiv:2403.07197

work page arXiv 2024
[31]

Equiv- alence checking of quantum circuits by model counting

Jingyi Mei, Tim Coopmans, Marcello Bonsangue, and Alfons Laarman. Equiv- alence checking of quantum circuits by model counting. InInternational Joint Conference on Automated Reasoning, pages 401–421. Springer, 2024

2024
[32]

Disentangling the gap between quantum and# sat

Jingyi Mei, Jan Martens, and Alfons Laarman. Disentangling the gap between quantum and# sat. InInternational Colloquium on Theoretical Aspects of Com- puting, pages 17–40. Springer, 2024

2024
[33]

Sympy: symbolic computing in python.PeerJ Computer Science, 3:e103, 2017

Aaron Meurer, Christopher P Smith, Mateusz Paprocki, Ondˇ rej ˇCert´ ık, Sergey B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K Moore, Sartaj Singh, et al. Sympy: symbolic computing in python.PeerJ Computer Science, 3:e103, 2017

2017
[34]

Nielsen and Isaac Chuang.Quantum computation and quantum infor- mation

Michael A. Nielsen and Isaac Chuang.Quantum computation and quantum infor- mation. Cambridge University Press, Cambridge, United Kingdom, 2002

2002
[35]

Equivalence checking of pa- rameterized quantum circuits: Verifying the compilation of variational quantum algorithms

Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of pa- rameterized quantum circuits: Verifying the compilation of variational quantum algorithms. InProceedings of the 28th Asia and South Pacific Design Automation Conference, ASPDAC ’23, page 702–708, New York, NY, USA, 2023. Association for Computing Machinery

2023
[36]

MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing.Quantum, 2023

Nils Quetschlich, Lukas Burgholzer, and Robert Wille. MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing.Quantum, 2023. MQT Bench is available athttps://www.cda.cit.tum.de/mqtbench/

2023
[37]

Quantum circuit equivalence checking: A tractable bridge from unitary to hybrid circuits

J´ erome Ricciardi, S´ ebastien Bardin, Christophe Chareton, and Benoˆ ıt Valiron. Quantum circuit equivalence checking: A tractable bridge from unitary to hybrid circuits. In3rd International Workshop on Services and Quantum Software, 2025

2025
[38]

Symbolic quantum simula- tion with quasimodo

Meghana Sistla, Swarat Chaudhuri, and Thomas Reps. Symbolic quantum simula- tion with quasimodo. InInternational Conference on Computer Aided Verification, pages 213–225. Springer, 2023

2023
[39]

Improvement of projected model-counting solver with component decomposition using sat solving in compo- nents

Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai. Improvement of projected model-counting solver with component decomposition using sat solving in compo- nents. Technical report, Technical report, JSAI Technical Report, SIG-FPAI-103- B506, 2017

2017
[40]

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

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

2010
[41]

The structure of sum-over-paths, its consequences, and complete- ness for clifford

Renaud Vilmart. The structure of sum-over-paths, its consequences, and complete- ness for clifford. InFoundations of Software Science and Computation Structures, volume 12650, page 531, 2021

2021
[42]

Rewriting and completeness of sum-over-paths in dyadic frag- ments of quantum computing.Logical Methods in Computer Science, Volume 20, Issue 1, March 2024

Renaud Vilmart. Rewriting and completeness of sum-over-paths in dyadic frag- ments of quantum computing.Logical Methods in Computer Science, Volume 20, Issue 1, March 2024

2024
[43]

Ac- curate bdd-based unitary operator manipulation for scalable and robust quantum circuit verification

Chun-Yu Wei, Yuan-Hung Tsai, Chiao-Shan Jhang, and Jie-Hong R Jiang. Ac- curate bdd-based unitary operator manipulation for scalable and robust quantum circuit verification. InProceedings of the 59th ACM/IEEE Design Automation Conference, pages 523–528, 2022

2022