pith. sign in

arxiv: 2605.16509 · v1 · pith:T56BOUE7new · submitted 2026-05-15 · 🪐 quant-ph

Quokka#: Quantum Computing with #SAT

Jingyi Mei , Dekel Zak , Muhammad Osama , Tim Coopmans , Alfons Laarman This is my paper

Pith reviewed 2026-05-20 18:51 UTC · model grok-4.3

classification 🪐 quant-ph
keywords quantum circuits#SATweighted model countingcircuit synthesisequivalence checkingquantum verificationgate set translationdepth optimization
0
0 comments X

The pith

Quokka# reduces quantum circuit simulation, verification, and synthesis tasks to weighted model counting while adding approximate equivalence checking for depth-optimal results across gate sets.

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

The paper presents Quokka#, a Python library that converts standard quantum circuit problems into weighted model counting instances, also called #SAT. This reduction lets existing solvers tackle simulation, verification, and synthesis without building custom quantum simulators for each job. The library supplies several encodings based on different algebraic bases, letting users trade accuracy for speed. Adding approximate equivalence checking is key because it supports translation between arbitrary gate sets while keeping the synthesis engine depth-optimal. A reader would care if this approach scales, because it could let engineers verify and optimize practical quantum programs using mature classical counting tools.

Core claim

Quokka# encodes universal quantum circuits and a wide range of gates into weighted model counting problems. It supplies multiple encodings that create performance trade-offs and introduces approximate equivalence checking to drive depth-optimal synthesis between arbitrary gate sets. The library is open-source and designed to handle real-world quantum computing tasks through these reductions.

What carries the argument

Reduction of quantum circuit tasks to weighted model counting (#SAT) through multiple algebraic encodings, plus approximate equivalence checking that enables depth-optimal synthesis between arbitrary gate sets.

If this is right

  • Verification of quantum circuits can reuse any off-the-shelf weighted model counter instead of quantum-specific simulators.
  • Synthesis can produce depth-optimal circuits even when the source and target gate sets differ completely.
  • Users can select among encodings to balance precision against running time for different circuit sizes.
  • The same framework can be extended to new gate types without rewriting the core counting engine.
  • Depth-optimal results become available for practical quantum programs that mix gates from several libraries.

Where Pith is reading between the lines

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

  • If #SAT solvers continue to improve, the same reductions could handle circuits with more qubits than current direct simulators allow.
  • Approximate equivalence checking might be reused outside synthesis for faster debugging of large quantum programs.
  • The library could serve as a bridge that lets classical verification researchers test ideas directly on quantum examples.
  • Testing the approach on error-corrected circuits would show whether the method remains useful when gates include error models.

Load-bearing premise

The encodings must correctly preserve the meaning of quantum operations and the resulting #SAT problems must remain small enough for solvers to finish in reasonable time.

What would settle it

Apply Quokka# to a small, known-optimal circuit such as a 3-qubit Toffoli and check whether the synthesized depth matches the known minimum while the output state distribution stays equivalent within the stated approximation.

Figures

Figures reproduced from arXiv: 2605.16509 by Alfons Laarman, Dekel Zak, Jingyi Mei, Muhammad Osama, Tim Coopmans.

Figure 1
Figure 1. Figure 1: The architecture of Quokka#. verification, equivalence checking, and synthesis, with their inputs and outputs. Quokka# understands quantum circuits in QASM format [40]. Its circuit encoder transforms the circuits to a Boolean formula with weights on literals as explained in Section 4. The different engines instrument the encoding to implement the desired functionality (as detailed in Section 5). After inst… view at source ↗
read the original abstract

We present Quokka#, a versatile, open-source Python library for quantum circuit analysis. Quokka# reduces various simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. Quokka# provides multiple encodings based on different algebraic bases and equivalence-checking methods, enabling key performance trade-offs. Moreover, the new version of Quokka# adds approximate equivalence checking, which is crucial in its synthesis algorithms, since it enables translation between arbitrary gate sets. Its synthesis engine is depth-optimal, making it well-suited to real-world quantum computing. This paper demonstrates the design, extensibility, and use of Quokka#.

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.

Referee Report

2 major / 1 minor

Summary. The paper presents Quokka#, an open-source Python library for quantum circuit analysis that reduces simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal circuits and a wide variety of gates via multiple encodings based on different algebraic bases, enabling performance trade-offs. The updated version adds approximate equivalence checking to support synthesis between arbitrary gate sets, and the synthesis engine is claimed to be depth-optimal. The manuscript focuses on the library's design, extensibility, and usage examples.

Significance. If the encodings preserve semantics and the approximate equivalence method reliably yields depth-optimal results, Quokka# could provide a practical, extensible tool for quantum circuit tasks by leveraging #SAT solvers. The support for trade-offs across encodings and open-source availability are strengths that could facilitate adoption in verification and optimization workflows.

major comments (2)
  1. [Synthesis section] Synthesis section: the claim that approximate equivalence checking enables depth-optimal synthesis between arbitrary gate sets lacks an explicit error bound or proof showing that the approximation threshold preserves minimality of circuit depth; without this, deviations could undermine the optimality guarantee.
  2. [Encodings section] Encodings section: the reductions of circuit semantics to weighted model counting are asserted to be correct for the supported gates and algebraic bases, but no formal argument, small-case verification, or semantic-preservation lemma is supplied to confirm this for universal circuits.
minor comments (1)
  1. [Abstract] The abstract states that encodings enable 'key performance trade-offs' but does not enumerate them or point to the relevant later section or table.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback. We address each major comment point by point below.

read point-by-point responses

  1. Referee: [Synthesis section] Synthesis section: the claim that approximate equivalence checking enables depth-optimal synthesis between arbitrary gate sets lacks an explicit error bound or proof showing that the approximation threshold preserves minimality of circuit depth; without this, deviations could undermine the optimality guarantee.

    Authors: We acknowledge that the manuscript does not supply an explicit error bound or formal proof that the chosen approximation threshold in equivalence checking preserves depth minimality for arbitrary gate sets. The depth-optimality claim applies to the specific synthesis procedure described, where the threshold is selected to avoid false negatives in practice. To address the concern, we will revise the Synthesis section to include a discussion of the threshold, its derivation from the underlying counting method, and supporting empirical evidence from benchmarks that the resulting circuits remain minimal in depth. revision: yes

  2. Referee: [Encodings section] Encodings section: the reductions of circuit semantics to weighted model counting are asserted to be correct for the supported gates and algebraic bases, but no formal argument, small-case verification, or semantic-preservation lemma is supplied to confirm this for universal circuits.

    Authors: The referee is correct that the current text asserts correctness of the reductions without a formal semantic-preservation lemma or dedicated small-case verification. The encodings follow directly from the chosen algebraic bases, and their behavior is validated through the library implementation. In the revised manuscript we will add a concise semantic-preservation argument for the supported gates together with explicit verification results on small universal circuits to confirm the reductions. revision: yes

Circularity Check

0 steps flagged

No circularity: paper describes software library and encodings without self-referential derivations or fitted predictions

full rationale

The manuscript presents Quokka# as a Python library that reduces quantum circuit tasks to weighted model counting via explicit encodings based on algebraic bases. No derivation chain is claimed that reduces a 'prediction' or optimality result to its own fitted inputs or self-citations by construction. The synthesis engine is stated to be depth-optimal due to the reduction and approximate equivalence checking, but this is presented as an engineering feature of the tool rather than a mathematical theorem whose proof loops back to the paper's own assumptions. The work is self-contained as a software artifact description; external #SAT solvers and standard circuit semantics provide the independent foundation. No load-bearing self-citation chains or ansatz smuggling appear in the provided text.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The paper is a software tool description with no new physical or mathematical axioms, free parameters, or invented entities; it builds on standard concepts from quantum computing and #SAT solving.

pith-pipeline@v0.9.0 · 5641 in / 1115 out tokens · 49849 ms · 2026-05-20T18:51:18.459778+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

108 extracted references · 108 canonical work pages · 1 internal anchor

  1. [1]

    DIMACS CNF.https://jix.github.io/varisat/manual/0.2.0/formats/ dimacs.html, accessed: 2025-01-27

    work page 2025

  2. [2]

    GPMC extended with complex weights.https://github.com/ System-Verification-Lab/GPMC.git, accessed: 2026-01-26

    work page 2026

  3. [3]

    In: Computational Complexity Conference

    Aaronson, S., Chen, L.: Complexity-theoretic foundations of quantum supremacy experiments. In: Computational Complexity Conference. pp. 1–67 (2017).https: //doi.org/10.4230/LIPIcs.CCC.2017.22

    work page doi:10.4230/lipics.ccc.2017.22 2017

  4. [4]

    Proceedings of the ACM on Programming Languages9(POPL) (Jan 2025).https://doi.org/10.1145/3704868

    Abdulla, P.A., Chen, Y.G., Chen, Y.F., Hol´ ık, L., Leng´ al, O., Lin, J.A., Lo, F.Y., Tsai, W.L.: Verifying quantum circuits with level-synchronized tree au- tomata. Proceedings of the ACM on Programming Languages9(POPL) (Jan 2025).https://doi.org/10.1145/3704868

    work page doi:10.1145/3704868 2025

  5. [5]

    Electronic Proceedings in Theoretical Computer Science287, 121 (Jan 2019)

    Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electronic Proceedings in Theoretical Computer Science287, 121 (Jan 2019). https://doi.org/10.4204/eptcs.287.1

    work page doi:10.4204/eptcs.287.1 2019

  6. [6]

    Electronic Proceedings in Theoretical Computer Science394, 343362 (Nov 2023).https://doi.org/10.4204/eptcs.394.17

    Amy, M., Bennett-Gibbs, O., Ross, N.J.: Symbolic synthesis of Clifford circuits and beyond. Electronic Proceedings in Theoretical Computer Science394, 343362 (Nov 2023).https://doi.org/10.4204/eptcs.394.17

    work page doi:10.4204/eptcs.394.17 2023

  7. [7]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems32(6), 818–830 (2013).https://doi.org/10.1109/TCAD.2013.2244643

    Amy, M., Maslov, D., Mosca, M., Roetteler, M.: A meet-in-the-middle algo- rithm for fast synthesis of depth-optimal quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems32(6), 818–830 (2013).https://doi.org/10.1109/TCAD.2013.2244643

    work page doi:10.1109/tcad.2013.2244643 2013

  8. [8]

    Physical Review A73(2) (Feb 2006).https://doi.org/10.1103/ physreva.73.022334

    Anders, S., Briegel, H.J.: Fast simulation of stabilizer circuits using a graph-state representation. Physical Review A73(2) (Feb 2006).https://doi.org/10.1103/ physreva.73.022334

    work page 2006

  9. [9]

    In: Meel, K.S., Strichman, O

    Audemard, G., Lagniez, J.M., Miceli, M.: A new exact solver for (weighted) Max#SAT. In: Meel, K.S., Strichman, O. (eds.) Theory and Applications of Satisfiability Testing. Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp. 28:1–28:20. Schloss Dagstuhl – Leibniz-Zentrum f¨ ur Informatik, Dagstuhl, Germany (2022).https://doi.org/10.423...

    work page doi:10.4230/lipics.sat.2022.28 2022

  10. [10]

    In: Chechik, M., Katoen, J.P., Leucker, M

    Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: Automated symbolic verifi- cation of Quantum Programs. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) Formal Methods. pp. 181–198. Springer International Publishing, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_12

    work page doi:10.1007/978-3-031-27481-7_12 2023

  11. [11]

    In: Conference on Uncertainty in Artificial Intelligence

    Beame, P., Li, J., Roy, S., Suciu, D.: Lower bounds for exact model counting and applications in probabilistic databases. In: Conference on Uncertainty in Artificial Intelligence. pp. 52–61 (2013).https://doi.org/10.5555/3023638.3023644

    work page doi:10.5555/3023638.3023644 2013

  12. [12]

    Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2022).https://doi.org/10.4230/ LIPICS.SAT.2022.18

    Berent, L., Burgholzer, L., Wille, R.: Towards a SAT encoding for quantum cir- cuits: A journey from classical circuits to Clifford circuits and beyond. Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik (2022).https://doi.org/10.4230/ LIPICS.SAT.2022.18

    work page 2022

  13. [13]

    In: ACM symposium on Theory of computing

    Bernstein, E., Vazirani, U.: Quantum complexity theory. In: ACM symposium on Theory of computing. pp. 11–20 (1993).https://doi.org/10.1145/167088. 167097

    work page doi:10.1145/167088 1993

  14. [14]

    Handbook of satisfiability185(99), 457–481 (2009) 13

    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Handbook of satisfiability185(99), 457–481 (2009) 13

    work page 2009

  15. [15]

    In: Computer Aided Verification

    Birgmeier, J., Bradley, A.R., Weissenbacher, G.: Counterexample to induction- guided abstraction-refinement (CTIGAR). In: Computer Aided Verification. Lec- ture Notes in Computer Science, vol. 8559, pp. 831–848. Springer (2014).https: //doi.org/10.1007/978-3-319-08867-9_55

    work page doi:10.1007/978-3-319-08867-9_55 2014

  16. [16]

    In: International Workshop on Verification, Model Checking, and Abstract Interpretation

    Bradley, A.R.: SAT-based model checking without unrolling. In: International Workshop on Verification, Model Checking, and Abstract Interpretation. pp. 70–

    work page

  17. [17]

    Springer (2011).https://doi.org/10.1007/978-3-642-18275-4_7

    work page doi:10.1007/978-3-642-18275-4_7 2011

  18. [18]

    In: Theory and Applications of Satisfiability Testing

    Brand, S., Coopmans, T., Laarman, A.: Quantum graph-state synthesis with SAT. In: Theory and Applications of Satisfiability Testing. CEUR Workshop Proceedings, vol. 3545, pp. 1–13. CEUR-WS.org (2023),https://ceur-ws.org/ Vol-3545/paper1.pdf

    work page 2023

  19. [19]

    In: International Symposium on Automated Technology for Ver- ification and Analysis

    Brand, S., Laarman, A.: Q-sylvan: a parallel decision diagram package for quan- tum computing. In: International Symposium on Automated Technology for Ver- ification and Analysis. pp. 260–273. Springer (2025).https://doi.org/10.1007/ 978-3-032-08707-2_12

    work page 2025

  20. [20]

    In: International Confer- ence on Quantitative Evaluation of Systems and Formal Modeling and Analy- sis of Timed Systems

    Brand, S., Quist, A.J., van Dijk, R.M., Laarman, A.: Numerical errors in quantitative system analysis with decision diagrams. In: International Confer- ence on Quantitative Evaluation of Systems and Formal Modeling and Analy- sis of Timed Systems. pp. 371–388. Springer (2025).https://doi.org/10.1007/ 978-3-032-05792-1_20

    work page 2025

  21. [21]

    Quantum3, 181 (Sep 2019).https://doi.org/10.22331/q-2019-09-02-181

    Bravyi, S., Browne, D., Calpin, P., Campbell, E., Gosset, D., Howard, M.: Sim- ulation of quantum circuits by low-rank stabilizer decompositions. Quantum3, 181 (Sep 2019).https://doi.org/10.22331/q-2019-09-02-181

    work page doi:10.22331/q-2019-09-02-181 2019

  22. [22]

    Quantum5, 580 (Nov 2021).https://doi

    Bravyi, S., Shaydulin, R., Hu, S., Maslov, D.: Clifford circuit optimization with templates and symbolic Pauli gates. Quantum5, 580 (Nov 2021).https://doi. org/10.22331/q-2021-11-16-580

    work page doi:10.22331/q-2021-11-16-580 2021

  23. [23]

    Physics Review X6, 021043 (Jun 2016).https://doi.org/10.1103/ PhysRevX.6.021043

    Bravyi, S., Smith, G., Smolin, J.A.: Trading classical and quantum computational resources. Physics Review X6, 021043 (Jun 2016).https://doi.org/10.1103/ PhysRevX.6.021043

    work page 2016

  24. [24]

    IEEE Transactions on Computers35(8), 677–691 (1986).https://doi.org/10.1109/ TC.1986.1676819

    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers35(8), 677–691 (1986).https://doi.org/10.1109/ TC.1986.1676819

    work page arXiv 1986

  25. [25]

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

    Bryant, R.E.: Numerical considerations in weighted model counting (2025). https://doi.org/10.48550/arXiv.2508.06264

    work page doi:10.48550/arxiv.2508.06264 2025

  26. [26]

    In: Asia and South Pacific Design Automation Confer- ence

    Burgholzer, L., Kueng, R., Wille, R.: Random stimuli generation for the verifica- tion of quantum circuits. In: Asia and South Pacific Design Automation Confer- ence. pp. 767–772 (2021).https://doi.org/10.1145/3394885.3431590

    work page doi:10.1145/3394885.3431590 2021

  27. [27]

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

    Burgholzer, L., Wille, R.: Improved DD-based equivalence checking of quan- tum circuits. In: 2020 25th Asia and South Pacific Design Automation Con- ference (ASP-DAC). pp. 127–132. IEEE (2020).https://doi.org/10.1109/ ASP-DAC47756.2020.9045153

    work page arXiv 2020

  28. [28]

    IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (Sep 2021).https://doi.org/10.1109/tcad.2020.3032630

    Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810–1824 (Sep 2021).https://doi.org/10.1109/tcad.2020.3032630

    work page doi:10.1109/tcad.2020.3032630 2021

  29. [29]

    In: Handbook of Model Checking, pp

    Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. In: Handbook of Model Checking, pp. 219–245. Springer (2018).https://doi.org/10.1007/ 978-3-319-10575-8_8

    work page 2018

  30. [30]

    In: International Joint Conference on Artificial Intelligence

    Chakraborty, S., Fried, D., Meel, K.S., Vardi, M.Y.: From weighted to unweighted model counting. In: International Joint Conference on Artificial Intelligence. pp. 689–695 (2015).https://doi.org/10.5555/2832249.2832345 14

    work page doi:10.5555/2832249.2832345 2015

  31. [31]

    Artificial Intelligence172(6), 772–799 (2008).https: //doi.org/10.1016/j.artint.2007.11.002,https://www.sciencedirect

    Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artificial Intelligence172(6), 772–799 (2008).https: //doi.org/10.1016/j.artint.2007.11.002,https://www.sciencedirect. com/science/article/pii/S0004370207001889

    work page doi:10.1016/j.artint.2007.11.002 2008

  32. [32]

    Association for Computing Machinery, New York, NY, USA (2025).https:// doi.org/10.1145/3676536.3676711

    Chen, T.F., Chen, Y.F., Jiang, J.H.R., Jobranov´ a, S., Leng´ al, O.: Accelerating Quantum Circuit Simulation with Symbolic Execution and Loop Summarization. Association for Computing Machinery, New York, NY, USA (2025).https:// doi.org/10.1145/3676536.3676711

    work page doi:10.1145/3676536.3676711 2025

  33. [33]

    In: Gurfinkel, A., Heule, M

    Chen, T.F., Jiang, J.H.R.: SliQSim: A quantum circuit simulator and solver for probability and statistics queries. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 129–

    work page

  34. [34]

    Springer Nature Switzerland, Cham (2025).https://doi.org/10.1007/ 978-3-031-90660-2_7

    work page 2025

  35. [35]

    Variational quantum pulse learning,

    Chen, T.F., Jiang, J.H.R., Hsieh, M.H.: Partial equivalence checking of quan- tum circuits. In: IEEE International Conference on Quantum Computing and Engineering (QCE). pp. 594–604. IEEE (2022).https://doi.org/10.1109/ QCE53715.2022.00082

    work page arXiv 2022

  36. [36]

    In: Gurfinkel, A., Heule, M

    Chen, Y.F., Chung, K.M., Hsieh, M.H., Huang, W.J., Leng´ al, O., Lin, J.A., Tsai, W.L.: AutoQ 2.0: From verification of quantum circuits to verification of quan- tum programs. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 87–108. Springer Nature Switzerland, Cham (2025).https://doi.org/10.1007/9...

    work page doi:10.1007/978-3-031-90660-2_5 2025

  37. [37]

    In: Computer Aided Verification

    Chen, Y.F., Chung, K.M., Leng´ al, O., Lin, J.A., Tsai, W.L.: AutoQ: An automata- based quantum circuit verifier. In: Computer Aided Verification. pp. 139–153. Springer (2023).https://doi.org/10.1007/978-3-031-37709-9_7

    work page doi:10.1007/978-3-031-37709-9_7 2023

  38. [38]

    Chen, Y.F., Chung, K.M., Leng´ al, O., Lin, J.A., Tsai, W.L., Yen, D.D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang.7(PLDI) (jun 2023).https://doi.org/10.1145/ 3591270

    work page 2023

  39. [39]

    In: International Conference on Au- tomated Deduction

    Chen, Y.F., R¨ ummer, P., Tsai, W.L.: A theory of cartesian arrays (with ap- plications in quantum circuit verification). In: International Conference on Au- tomated Deduction. pp. 170–189. Springer (2023).https://doi.org/10.1007/ 978-3-031-38499-8_10

    work page 2023

  40. [40]

    Linear Al- gebra and its Applications10(3), 285–290 (1975).https://doi.org/10.1016/ 0024-3795(75)90075-0

    Choi, M.D.: Completely positive linear maps on complex matrices. Linear Al- gebra and its Applications10(3), 285–290 (1975).https://doi.org/10.1016/ 0024-3795(75)90075-0

    work page 1975

  41. [41]

    New Journal of Physics13(4), 043016 (2011).https://doi.org/ 10.1088/1367-2630/13/4/043016

    Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics13(4), 043016 (2011).https://doi.org/ 10.1088/1367-2630/13/4/043016

    work page doi:10.1088/1367-2630/13/4/043016 2011

  42. [42]

    ACM Transac- tions on Quantum Computing3(3), 150 (Sep 2022).https://doi.org/10.1145/ 3505636

    Cross, A., Javadi-Abhari, A., Alexander, T., De Beaudrap, N., Bishop, L.S., Hei- del, S., Ryan, C.A., Sivarajah, P., Smolin, J., Gambetta, J.M., Johnson, B.R.: OpenQASM3: A broader and deeper quantum assembly language. ACM Transac- tions on Quantum Computing3(3), 150 (Sep 2022).https://doi.org/10.1145/ 3505636

    work page 2022

  43. [43]

    13 Adnan Darwiche and Pierre Marquis

    Darwiche, A., Marquis, P.: A knowledge compilation map. Journal of Artificial Intelligence Research17, 229–264 (2002).https://doi.org/10.1613/jair.989

    work page doi:10.1613/jair.989 2002

  44. [44]

    Quantum Inf

    Dawson, C.M., Nielsen, M.A.: The Solovay-Kitaev algorithm. Quantum Inf. Com- put.6(1), 81–95 (2006).https://doi.org/10.26421/QIC6.1-6

    work page doi:10.26421/qic6.1-6 2006

  45. [45]

    doi: 10.1016/j

    de Campos, C.P., Stamoulis, G., Weyland, D.: A structured view on weighted counting with relations to counting, quantum computation and applications. In- 15 formation and Computation275, 104627 (2020).https://doi.org/10.1016/j. ic.2020.104627

    work page doi:10.1016/j 2020

  46. [46]

    In: International Static Analysis Symposium

    Donaldson, A.F., Haller, L., Kroening, D., R¨ ummer, P.: Software verification using k-induction. In: International Static Analysis Symposium. pp. 351–368. Springer (2011).https://doi.org/10.1007/978-3-642-23702-7_26

    work page doi:10.1007/978-3-642-23702-7_26 2011

  47. [47]

    In: Formal Methods in Computer-Aided Design

    Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property di- rected reachability. In: Formal Methods in Computer-Aided Design. pp. 125–134. FMCAD Inc (2011)

    work page 2011

  48. [48]

    Quantum Physics using Weighted Model Counting

    Ende, D.v.d., Lee, J.H., Laarman, A.: Quantum physics using weighted model counting. arXiv preprint arXiv:2508.21288 (2025).https://doi.org/10.48550/ arXiv.2508.21288

    work page internal anchor Pith review Pith/arXiv arXiv 2025

  49. [49]

    International Journal of The- oretical Physics21(6), 467–488 (1982).https://doi.org/10.1007/BF02650179

    Feynman, R.P.: Simulating physics with computers. International Journal of The- oretical Physics21(6), 467–488 (1982).https://doi.org/10.1007/BF02650179

    work page doi:10.1007/bf02650179 1982

  50. [50]

    Fichte, J.K., Hecher, M.: The model counting competitions 2021-2023 (2025), https://arxiv.org/abs/2504.13842

    work page arXiv 2021

  51. [51]

    Journal of Computer and System Sciences59(2), 240–252 (1999).https://doi.org/10

    Fortnow, L., Rogers, J.: Complexity limitations on quantum computation. Journal of Computer and System Sciences59(2), 240–252 (1999).https://doi.org/10. 1006/jcss.1999.1651

    work page arXiv 1999

  52. [52]

    Physical Review AAtomic, Molecular, and Optical Physics87(3), 032332 (2013).https: //doi.org/10.1103/PhysRevA.87.032332

    Giles, B., Selinger, P.: Exact synthesis of multiqubit Clifford+T circuits. Physical Review AAtomic, Molecular, and Optical Physics87(3), 032332 (2013).https: //doi.org/10.1103/PhysRevA.87.032332

    work page doi:10.1103/physreva.87.032332 2013

  53. [53]

    Hashimoto, K.: GPMC.https://git.trs.css.i.nagoya-u.ac.jp/k-hasimt/ GPMC(2020)

    work page 2020

  54. [54]

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

    Hong, X., Feng, Y., Li, S., Ying, M.: Equivalence checking of dynamic quantum circuits. In: IEEE/ACM International Conference on Computer-Aided Design. ICCAD ’22, Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3508352.3549479

    work page doi:10.1145/3508352.3549479 2022

  55. [55]

    In: ACM/IEEE Design Automation Con- ference

    Hong, X., Ying, M., Feng, Y., Zhou, X., Li, S.: Approximate equivalence checking of noisy quantum circuits. In: 2021 58th ACM/IEEE Design Automation Confer- ence. pp. 637–642 (2021).https://doi.org/10.1109/DAC18074.2021.9586214

    work page doi:10.1109/dac18074.2021.9586214 2021

  56. [56]

    Journal of Artificial Intelligence Research29, 191–219 (2007).https://doi.org/10.1613/jair.2097

    Huang, J., Darwiche, A.: The language of search. Journal of Artificial Intelligence Research29, 191–219 (2007).https://doi.org/10.1613/jair.2097

    work page doi:10.1613/jair.2097 2007

  57. [57]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Huang, W.J., Chareton, C., Chen, Y.F., Chung, K.M., Hsieh, M.H., Laarman, A., Mei, J.: Equivalence checking of quantum circuits via path-sum and weighted model counting. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 419–439. Springer (2026).https:// doi.org/10.1007/978-3-032-22749-2_21

    work page doi:10.1007/978-3-032-22749-2_21 2026

  58. [58]

    In: ACM inter- national conference on architectural support for programming languages and oper- ating systems

    Huang, Y., Holtzen, S., Millstein, T., Van den Broeck, G., Martonosi, M.: Logical abstractions for noisy variational quantum algorithm simulation. In: ACM inter- national conference on architectural support for programming languages and oper- ating systems. pp. 456–472 (2021).https://doi.org/10.1145/3445814.3446750

    work page doi:10.1145/3445814.3446750 2021

  59. [59]

    Jean-Marie Lagniez, M.M.: d4.https://github.com/crillab/d4v2(2024)

    work page 2024

  60. [60]

    Journal of Applied Logic22, 46–62 (2017).https://doi.org/10.1016/j.jal.2016.11

    Kimmig, A., Van den Broeck, G., De Raedt, L.: Algebraic model counting. Journal of Applied Logic22, 46–62 (2017).https://doi.org/10.1016/j.jal.2016.11. 031, sI:Uncertain Reasoning

    work page doi:10.1016/j.jal.2016.11 2017

  61. [61]

    In: Quantum Physics and Logic (QPL) (2019).https://doi.org/10

    Kissinger, A., van de Wetering, J.: PyZX: Large scale automated diagrammatic reasoning. In: Quantum Physics and Logic (QPL) (2019).https://doi.org/10. 4204/EPTCS.318.14

    work page 2019

  62. [62]

    Quantum Science and Technology7(4), 044001 (Jul 2022).https://doi.org/10.1088/2058-9565/ac5d20 16

    Kissinger, A., van de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quantum Science and Technology7(4), 044001 (Jul 2022).https://doi.org/10.1088/2058-9565/ac5d20 16

    work page doi:10.1088/2058-9565/ac5d20 2022

  63. [63]

    Korhonen, T., Jarvisalo, M.: SharpSAT-TD in model counting competitions 2021- 2023 (2023)

    work page 2021

  64. [64]

    McMillan, K.: Symbolic model checking: an approach to the state explosion prob- lem. Ph.D. thesis, Carnegie Mellon University (1992), uMI No. GAX92-24209

    work page 1992

  65. [65]

    In: IJ- CAI

    Meel, K.S.: Counting, sampling, and synthesis: The quest for scalability. In: IJ- CAI. pp. 5816–5820 (2022).https://doi.org/10.24963/ijcai.2022/817

    work page doi:10.24963/ijcai.2022/817 2022

  66. [66]

    In: Gurfinkel, A., Ganesh, V

    Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification. pp. 555–578. Springer Nature Switzerland, Cham (2024).https://doi.org/10.1007/ 978-3-031-65633-0_25

    work page 2024

  67. [67]

    In: Benzm¨ uller, C., Heule, M.J., Schmidt, R.A

    Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. In: Benzm¨ uller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning (IJCAR). pp. 401–421. Springer Nature Switzerland, Cham (2024).https://doi.org/10.1007/978-3-031-63501-4_21

    work page doi:10.1007/978-3-031-63501-4_21 2024

  68. [68]

    In: Anutariya, C., Bonsangue, M.M

    Mei, J., Martens, J., Laarman, A.: Disentangling the gap between quantum and #SAT. In: Anutariya, C., Bonsangue, M.M. (eds.) Theoretical Aspects of Com- puting – ICTAC 2024. pp. 17–40. Springer Nature Switzerland, Cham (2025). https://doi.org/10.1007/978-3-031-77019-7_2

    work page doi:10.1007/978-3-031-77019-7_2 2024

  69. [69]

    Quokka#: Quantum computing with #SAT

    Mei, J., Zak, D., Osama, M., Coopmans, T., Laarman, A.: Artifact for the CAV’26 paper “Quokka#: Quantum computing with #SAT” (2026).https://doi.org/ 10.5281/zenodo.19833587,https://zenodo.org/records/19833587

    work page doi:10.5281/zenodo.19833587 2026

  70. [70]

    PeerJ Computer Science 3, e103 (Jan 2017).https://doi.org/10.7717/peerj-cs.103

    Meurer, A., Smith, C.P., Paprocki, M., ˇCert´ ık, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., Rathnayake, T., Vig, S., Granger, B.E., Muller, R.P., Bonazzi, F., Gupta, H., Vats, S., Johansson, F., Pedregosa, F., Curry, M.J., Terrel, A.R., Rouˇ cka,ˇS., Saboo, A., Fernando, I., Kulal, S., Cimrman, R., Scopatz, A.: SymPy...

    work page doi:10.7717/peerj-cs.103 2017

  71. [71]

    In: International Symposium on Multiple-Valued Logic

    Miller, D.M., Thornton, M.A.: QMDD: A decision diagram structure for reversible and quantum circuits. In: International Symposium on Multiple-Valued Logic. pp. 30–30. IEEE (2006).https://doi.org/10.1109/ISMVL.2006.35

    work page doi:10.1109/ismvl.2006.35 2006

  72. [72]

    Cambridge University Press (2000).https://doi.org/10.1017/ CBO9780511976667

    Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum In- formation. Cambridge University Press (2000).https://doi.org/10.1017/ CBO9780511976667

    work page 2000

  73. [73]

    In: ACM SIGPLAN International Conference on Programming Language Design and Implementation

    Paradis, A., Bichsel, B., Steffen, S., Vechev, M.: Unqomp: synthesizing un- computation in quantum circuits. In: ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 222–236 (2021). https://doi.org/10.1145/3453483.3454040

    work page doi:10.1145/3453483.3454040 2021

  74. [74]

    Proceedings of the ACM on Programming Languages 8(OOPSLA1) (Apr 2024).https://doi.org/10.1145/3649813

    Paradis, A., Dekoninck, J., Bichsel, B., Vechev, M.: Synthetiq: Fast and versatile quantum circuit synthesis. Proceedings of the ACM on Programming Languages 8(OOPSLA1) (Apr 2024).https://doi.org/10.1145/3649813

    work page doi:10.1145/3649813 2024

  75. [75]

    Quantum7, 1062 (Jul 2023).https://doi.org/10.22331/q-2023-07-20-1062

    Quetschlich, N., Burgholzer, L., Wille, R.: MQT bench: Benchmarking software and design automation tools for quantum computing. Quantum7, 1062 (Jul 2023).https://doi.org/10.22331/q-2023-07-20-1062

    work page doi:10.22331/q-2023-07-20-1062 2023

  76. [76]

    arXiv preprint arXiv:2602.17775 (2026).https://doi.org/10.48550/arXiv.2602.17775

    Quist, A.J., Coopmans, T., Laarman, A.: Exact quantum decision diagrams with scaling guarantees for Clifford+T circuits and beyond. arXiv preprint arXiv:2602.17775 (2026).https://doi.org/10.48550/arXiv.2602.17775

    work page doi:10.48550/arxiv.2602.17775 2026

  77. [77]

    In: International Symposium on Formal Methods

    Quist, A.J., Mei, J., Coopmans, T., Laarman, A.: Advancing quantum computing with formal methods. In: International Symposium on Formal Methods. pp. 420–

    work page

  78. [78]

    Springer (2024).https://doi.org/10.1007/978-3-031-71177-0_25 17

    work page doi:10.1007/978-3-031-71177-0_25 2024

  79. [79]

    In: Interna- tional Conference on Theory and Applications of Satisfiability Testing (2004), https://api.semanticscholar.org/CorpusID:52027

    Sang, T., Bacchus, F., Beame, P., Kautz, H.A., Pitassi, T.: Combining com- ponent caching and clause learning for effective model counting. In: Interna- tional Conference on Theory and Applications of Satisfiability Testing (2004), https://api.semanticscholar.org/CorpusID:52027

    work page 2004

  80. [80]

    In: AAAI

    Sang, T., Beame, P., Kautz, H.A.: Performing Bayesian inference by weighted model counting. In: AAAI. vol. 5, pp. 475–481 (2005).https://doi.org/10. 5555/1619332.1619409

    work page arXiv 2005

Showing first 80 references.