pith. sign in

arxiv: 2508.21288 · v2 · submitted 2025-08-29 · 🪐 quant-ph · cond-mat.stat-mech· math-ph· math.MP

Quantum Physics using Weighted Model Counting

Dirck van den Ende , Joon Hyung Lee , Alfons Laarman , Henning Basold This is my paper

Pith reviewed 2026-05-18 21:10 UTC · model grok-4.3

classification 🪐 quant-ph cond-mat.stat-mechmath-phmath.MP
keywords weighted model countingDirac notationquantum physicspartition functionIsing modelPotts modeltype systemdenotational semantics
0
0 comments X

The pith

A framework converts Dirac notation into weighted model counting problems to solve quantum linear algebra tasks.

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

This paper develops a general method to express problems from quantum physics and linear algebra as instances of weighted model counting. It does so by creating a conversion framework for Dirac notation that includes a type system and denotational semantics to ensure the mapping is correct. An implementation in Python is provided and used to compute partition functions for the transverse-field Ising model and the Potts model. The goal is to allow general techniques from automated reasoning to be applied to a broad range of quantum problems rather than developing solutions for each case separately.

Core claim

The paper claims that linear algebraic problems in physics and quantum computing can be systematically expressed as weighted model counting instances through a framework that translates Dirac notation, built using a type system and denotational semantics.

What carries the argument

The Dirac notation to WMC conversion framework with its type system and denotational semantics that maps quantum states and operators to weighted counting problems.

If this is right

  • Partition functions of the transverse-field Ising model can be calculated using WMC.
  • Partition functions of the Potts model can be calculated using WMC.
  • Automated reasoning heuristics can be applied systematically to quantum physics problems.
  • A reusable general framework replaces per-instance approaches for quantum calculations.

Where Pith is reading between the lines

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

  • This approach might scale to more complex quantum systems by using efficient WMC solvers.
  • It could connect quantum mechanics computations with tools from constraint satisfaction and counting.
  • Future work might extend the framework to handle time evolution or measurement in quantum circuits.

Load-bearing premise

The type system and denotational semantics correctly map Dirac notation and linear algebra onto weighted model counting without losing quantum features or adding errors.

What would settle it

Computing the partition function of the transverse-field Ising model with the framework and finding a numerical result that differs from the known exact or simulated value.

Figures

Figures reproduced from arXiv: 2508.21288 by Alfons Laarman, Dirck van den Ende, Henning Basold, Joon Hyung Lee.

Figure 1
Figure 1. Figure 1: summarizes our framework pipeline: the user provides a physics problem and selects a WMC solver; the rest of the workflow is automated by our system. TF Ising model Potts model Physics problem Matrix problem DiracWMC DPMC Cachet TensorOrder Model counter Partition func. (or other qty.) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Diagram of multiplication operation on matrix representations. The sum of two matrices is represented in a similar way to scalars, with an extra variable that indicates which matrix should be evaluated. In this case, the input and output variables are also linked with the input and output variables of the respective matrix [PITH_FULL_IMAGE:figures/full_fig_p014_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Diagram of addition operation on matrix representations. The Kronecker product representation is constructed from the two independent representations of the matrices M1 and M2. The input and output variables of the two matrices are concatenated [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Diagram of Kronecker product operation on matrix representations. The multiplication of a scalar and a matrix can be represented by a conjunction of the two formulae. This operation uses the property that WMC(ϕ ∧ ψ, W1 ∪ W2) = WMC(ϕ, W1) · WMC(ψ, W2) for two formulae 14 [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: shows the operation schematically. Operation 9. Matrix-scalar multiplication JsKr = [(ϕs , Ws)] JMKr = [(ϕ, W, x, y, q)] dom(Ws) ∩ dom(W) = ∅    =⇒ Js · MKr = [(ϕ ∧ ϕs , W ∪ Ws , x, y, q)] (42) x M y s s · M [PITH_FULL_IMAGE:figures/full_fig_p016_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Diagram of the transpose of a matrix representation. Input and output variables are swapped. Applying a field endomorphism to a matrix is similar to applying it to a scalar. Operation 11. Field endomorphism on a matrix JMKr = [(ϕ, W, x, y, q)] =⇒ Japply(f , M)Kr = [(ϕ, f ◦ W, x, y, q)] (44) The trace of a matrix can be calculated by adding a clause to the conjunction requiring the input and output variable… view at source ↗
Figure 7
Figure 7. Figure 7: Diagram of taking the trace of a matrix, using a matrix representation to get a scalar representa￾tion. An entry in the matrix can be obtained by applying the definition from (26) directly. Instead of returning the quantity WMC(ϕ ∧ (x = j) ∧ (y = i), W), we return the model counting instance. Operation 13. Matrix entry JMKr = [(ϕ, W, x, y, q)] =⇒ Jentry(i, j, M)K = [(ϕ ∧ (x = j) ∧ (y = i), W)] (46) 3.7 Cor… view at source ↗
Figure 8
Figure 8. Figure 8: Runtime of calculating the partition func￾tion of an L × L square lattice Ising model with interaction strengths and external field strengths from the standard normal distribution, averaged over five runs. The problem is converted to a ma￾trix representation from Chapter 3, after which the trace is calculated using a model counter. Compar￾ison between the model counters Cachet, DPMC, and TensorOrder. Direc… view at source ↗
Figure 10
Figure 10. Figure 10: Runtime vs. relative error for TFIM partition function estimation using DPMC and Trotteriza￾tion. Random graphs with Gaussian couplings. Only DPMC runtime is reported. 10−3 10−2 10−1 100 101 Runtime (s) n = 2 n = 6 n = 10 n = 4 n = 8 n = 12 [PITH_FULL_IMAGE:figures/full_fig_p023_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Runtime of SciPy expm method for TFIM partition function. Uses same y-axis scale as [PITH_FULL_IMAGE:figures/full_fig_p023_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Runtime comparison of model counters on standard Potts models. Logarithmic encoding, 5 runs averaged, edge degree 4. Discussion. If only a few Jij(si ,sj) are nonzero, this encoding is tractable. In general, the standard Potts encoding is more compact, requiring fewer clauses than the generalized form, and can be more efficiently compiled. 7 Related work 7.1 D-Hammer Xu et al. [41] introduced D-Hammer: A … view at source ↗
Figure 13
Figure 13. Figure 13: Encoding comparison on Potts partition computation using DPMC. Log encoding outperforms at higher q. 7.3 Quantum circuit simulation using WMC Mei et al. [19, 20] showed that model counting can be used in quantum computing for simulating circuits and equivalence checking. They showed that quantum states can be encoded using variables [21]. Gates can then be encoded by expressing a relationship between inpu… view at source ↗
read the original abstract

Weighted model counting (WMC) has proven effective at a range of tasks within computer science, physics, and beyond. However, existing approaches for using WMC in quantum physics only target specific problem instances, lacking a general framework for expressing problems using WMC. This limits the reusability of these approaches in other applications and risks a lack of mathematical rigor on a per-instance basis. We present an approach for expressing linear algebraic problems, specifically those present in physics and quantum computing, as WMC instances. We do this by introducing a framework that converts Dirac notation to WMC problems. We build up this framework theoretically, using a type system and denotational semantics, and provide an implementation in Python. We demonstrate the effectiveness of our framework in calculating the partition functions of several physical models: The transverse-field Ising model (quantum) and the Potts model (classical). The results suggest that heuristics developed in automated reasoning can be systematically applied to a wide class of problems in quantum physics through our framework.

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 / 2 minor

Summary. The manuscript presents a framework for expressing linear algebraic problems from quantum physics and computing as weighted model counting (WMC) instances. It converts Dirac notation to WMC problems via a type system and denotational semantics, includes a Python implementation, and demonstrates the approach by computing partition functions for the transverse-field Ising model and the Potts model.

Significance. If the central mapping holds without loss of quantum structure or introduction of approximation errors, the work would enable systematic reuse of automated reasoning heuristics and solvers across a broad class of quantum physics problems, increasing both applicability and rigor compared to ad-hoc per-instance encodings.

major comments (2)
  1. [§3] §3 (Theoretical Framework): The denotational semantics are constructed from first principles, but the manuscript provides no explicit theorem or inductive proof establishing that the mapping from arbitrary Dirac expressions (including superpositions and tensor products) to WMC instances is exact and structure-preserving for the full class of linear-algebraic operations claimed. This is load-bearing for the generality assertion.
  2. [§5] §5 (Demonstrations): The reported results for the transverse-field Ising model and Potts model lack baseline comparisons (e.g., to exact diagonalization or standard Monte Carlo) and error analysis, so it is not possible to quantify whether the WMC encoding introduces any overhead or deviation from known values.
minor comments (2)
  1. [§4] The Python implementation is referenced but not included as supplementary material or pseudocode; adding it would support reproducibility.
  2. [§3.1] Notation for the translation of inner products and normalization constants into WMC weights could be made more explicit with a small worked example early in the text.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive and detailed comments. We address each major comment below and describe the revisions that will be incorporated into the next version of the manuscript.

read point-by-point responses

  1. Referee: [§3] §3 (Theoretical Framework): The denotational semantics are constructed from first principles, but the manuscript provides no explicit theorem or inductive proof establishing that the mapping from arbitrary Dirac expressions (including superpositions and tensor products) to WMC instances is exact and structure-preserving for the full class of linear-algebraic operations claimed. This is load-bearing for the generality assertion.

    Authors: We thank the referee for this observation. The denotational semantics in Section 3 are defined inductively over the grammar of Dirac expressions, with each production (scalars, kets, bras, tensor products, linear combinations, and adjoints) mapped compositionally to the corresponding WMC operations. This construction ensures that the linear-algebraic structure is preserved exactly, with no approximation or loss of quantum features. Nevertheless, we agree that stating an explicit theorem and providing an inductive argument would strengthen the presentation. In the revised manuscript we will insert a formal theorem in Section 3 asserting that the semantics is faithful and structure-preserving, together with a concise inductive proof sketch. revision: yes

  2. Referee: [§5] §5 (Demonstrations): The reported results for the transverse-field Ising model and Potts model lack baseline comparisons (e.g., to exact diagonalization or standard Monte Carlo) and error analysis, so it is not possible to quantify whether the WMC encoding introduces any overhead or deviation from known values.

    Authors: We agree that empirical validation against established methods would improve the evaluation section. Although the framework is exact by construction, we will add direct comparisons for small lattices: exact diagonalization results for the transverse-field Ising model and exhaustive enumeration for the Potts model. These baselines will be reported alongside the WMC-derived partition functions, together with a discussion of numerical agreement (expected to be exact within floating-point precision) and the relative computational cost of the WMC encoding versus the baselines. The revised Section 5 will include these comparisons and an accompanying error analysis. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected in framework construction

full rationale

The paper introduces a mapping from Dirac notation to weighted model counting via an explicitly defined type system and denotational semantics, which are built from first principles rather than derived from fitted data or prior self-referential results. Demonstrations compute partition functions for the transverse-field Ising model and Potts model using standard, externally known physical instances without post-hoc parameter adjustments or reductions that equate outputs to inputs by construction. The central contribution is a reusable framework with a Python implementation, and no load-bearing step relies on self-citation chains, uniqueness theorems from the same authors, or renaming of known results as novel derivations. This renders the derivation self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of the newly defined semantics mapping and the assumption that WMC can faithfully represent the linear algebra without loss for the chosen problem class. No free parameters or invented physical entities are introduced.

axioms (1)
  • domain assumption The denotational semantics correctly preserves the meaning of Dirac notation when mapped to weighted model counting.
    This mapping is the load-bearing step in the theoretical framework construction.

pith-pipeline@v0.9.0 · 5714 in / 1274 out tokens · 32398 ms · 2026-05-18T21:10:27.403753+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.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Quokka#: Quantum Computing with #SAT

    quant-ph 2026-05 unverdicted novelty 6.0

    Quokka# is a Python library that converts quantum circuit analysis tasks into #SAT problems, offering multiple encodings, approximate equivalence checking, and depth-optimal synthesis.

Reference graph

Works this paper leans on

43 extracted references · 43 canonical work pages · cited by 1 Pith paper

  1. [1]

    Ignasi Ab´ıo and Peter J. Stuckey. Encoding linear constraints into sat. In Barry O’Sullivan, editor, Principles and Practice of Constraint Programming, pages 75–91, Cham, 2014. Springer International Publishing

    work page 2014

  2. [2]

    Al-Mohy and Nicholas J

    Awad H. Al-Mohy and Nicholas J. Higham. A new scaling and squaring algorithm for the matrix exponential. SIAM Journal on Matrix Analysis and Applications, 31(3):970–989, 2010

    work page 2010

  3. [3]

    History of the lenz-ising model

    Stephen G Brush. History of the lenz-ising model. Reviews of modern physics, 39(4):883, 1967

    work page 1967

  4. [4]

    On probabilistic inference by weighted model counting

    Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6):772–799, 2008

    work page 2008

  5. [5]

    Interacting quantum observables: categorical algebra and diagram- matics

    Bob Coecke and Ross Duncan. Interacting quantum observables: categorical algebra and diagram- matics. New Journal of Physics, 13(4):043016, 4 2011

    work page 2011

  6. [6]

    scipy.linalg.expm, 2008

    The SciPy community. scipy.linalg.expm, 2008

    work page 2008

  7. [7]

    Pottics – the potts topic model for semantic image segmentation

    Christoph Dann, Peter Gehler, Stefan Roth, and Sebastian Nowozin. Pottics – the potts topic model for semantic image segmentation. In Proceedings of 34th DAGM Symposium, Lecture Notes in Computer Science, pages 397–407. Springer, August 2012

    work page 2012

  8. [8]

    Weighted model counting with conditional weights for bayesian networks

    Paulius Dilkas and Vaishak Belle. Weighted model counting with conditional weights for bayesian networks. In Cassio de Campos and Marloes H. Maathuis, editors, Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence , volume 161 of Proceedings of Machine Learning Research, pages 386–396. PMLR, 7 2021

    work page 2021

  9. [9]

    Diracwmc

    Dirck van den Ende. Diracwmc

    work page

  10. [10]

    Dudek, Vu H

    Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. Dpmc: Weighted model counting by dynamic programming on project-join trees. In Principles and Practice of Constraint Programming: 26th International Conference, CP 2020, Louvain-La-Neuve, Belgium, September 7–11, 2020, Proceedings, page 211–230, Berlin, Heidelberg, 2020. Springer-Verlag

    work page 2020

  11. [11]

    Dudek, Vu H

    Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. Procount: Weighted projected model counting with graded project-join trees. In Chu-Min Li and Felip Many`a, editors, Theory and Applications of Satisfiability Testing – SAT 2021, pages 152–170, Cham, 2021. Springer International Publishing

    work page 2021

  12. [12]

    Dudek and Moshe Y

    Jeffrey M. Dudek and Moshe Y. Vardi. Parallel weighted model counting with tensor networks, 2021

    work page 2021

  13. [13]

    H. B. Hunt and R. E. Stearns. On the complexity of satisfiability problems for algebraic structures (preliminary report). In Teo Mora, editor, Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, pages 250–258, Berlin, Heidelberg, 1989. Springer Berlin Heidelberg

    work page 1989

  14. [14]

    Efficient cnf encoding for selecting 1 from n objects

    William Klieber and Gihwon Kwon. Efficient cnf encoding for selecting 1 from n objects. 2007

    work page 2007

  15. [15]

    Efficient inference in fully connected crfs with gaussian edge potentials

    Philipp Kr¨ahenb ¨uhl and Vladlen Koltun. Efficient inference in fully connected crfs with gaussian edge potentials. In J. Shawe-Taylor, R. Zemel, P . Bartlett, F. Pereira, and K.Q. Weinberger, editors, Advances in Neural Information Processing Systems, volume 24. Curran Associates, Inc., 2011

    work page 2011

  16. [16]

    Potts hamiltonian models of protein co- variation, free energy landscapes, and evolutionary fitness.Curr Opin Struct Biol, 43:55–62, November 2016

    Ronald M Levy, Allan Haldane, and William F Flynn. Potts hamiltonian models of protein co- variation, free energy landscapes, and evolutionary fitness.Curr Opin Struct Biol, 43:55–62, November 2016

    work page 2016

  17. [17]

    Li, Mindren Lu, Israel Desta, Vikram Sundar, Gevorg Grigoryan, and Amy E

    Alex J. Li, Mindren Lu, Israel Desta, Vikram Sundar, Gevorg Grigoryan, and Amy E. Keating. Neural network-derived potts models for structure-based protein design using backbone atomic coordinates and tertiary motifs. Protein Science, 32(2):e4554, 2023. 42

    work page 2023

  18. [18]

    Quantum Neural Network Classifiers: A Tutorial

    Weikang Li, Zhide Lu, and Dong-Ling Deng. Quantum Neural Network Classifiers: A Tutorial. SciPost Phys. Lect. Notes, page 61, 2022

    work page 2022

  19. [19]

    Simulating quantum circuits by model counting

    Jingyi Mei, Marcello Bonsangue, and Alfons Laarman. Simulating quantum circuits by model counting. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification, pages 555–578, Cham, 2024. Springer Nature Switzerland

    work page 2024

  20. [20]

    Equivalence checking of quantum circuits by model counting

    Jingyi Mei, Tim Coopmans, Marcello Bonsangue, and Alfons Laarman. Equivalence checking of quantum circuits by model counting. In Christoph Benzm ¨uller, Marijn J.H. Heule, and Renate A. Schmidt, editors, Automated Reasoning, pages 401–421, Cham, 2024. Springer Nature Switzerland

    work page 2024

  21. [21]

    Disentangling the gap between quantum and #sat

    Jingyi Mei, Jan Martens, and Alfons Laarman. Disentangling the gap between quantum and #sat. In Theoretical Aspects of Computing – ICTAC 2024: 21st International Colloquium, Bangkok, Thailand, November 25–29, 2024, Proceedings, page 17–40, Berlin, Heidelberg, 2024. Springer-Verlag

    work page 2024

  22. [22]

    Dudek, Leonardo Due˜nas Osorio, and Moshe Y

    Shaan Nagy, Roger Paredes, Jeffrey M. Dudek, Leonardo Due˜nas Osorio, and Moshe Y. Vardi. Ising model partition-function computation as a weighted counting problem. Phys. Rev. E, 109:055301, 5 2024

    work page 2024

  23. [23]

    Empirical study on sat-encodings of the at-most-one constraint

    Van-Hau Nguyen, Van-Quyet Nguyen, Kyungbaek Kim, and Pedro Barahona. Empirical study on sat-encodings of the at-most-one constraint. In The 9th International Conference on Smart Media and Applications, SMA 2020, page 470–475, New York, NY, USA, 2021. Association for Computing Machinery

    work page 2020

  24. [24]

    A practical introduction to tensor networks: Matrix product states and projected entangled pair states

    Rom´an Or ´us. A practical introduction to tensor networks: Matrix product states and projected entangled pair states. Annals of Physics, 349:117–158, 2014

    work page 2014

  25. [25]

    Contracting arbitrary tensor networks: General approximate algorithm and applications in graphical models and quantum circuit simulations

    Feng Pan, Pengfei Zhou, Sujie Li, and Pan Zhang. Contracting arbitrary tensor networks: General approximate algorithm and applications in graphical models and quantum circuit simulations. Phys. Rev. Lett., 125:060503, 8 2020

    work page 2020

  26. [26]

    A weighted model counting approach for critical infras- tructure reliability, 5 2019

    Paredes, Due˜nas-Osorio, Meel, and Vardi. A weighted model counting approach for critical infras- tructure reliability, 5 2019

    work page 2019

  27. [27]

    Portela, George D.C

    Nara M. Portela, George D.C. Cavalcanti, and Tsang Ing Ren. Contextual image segmentation based on the potts model. In 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, pages 256–261, 2013

    work page 2013

  28. [28]

    Chapter 2

    Steven Prestwich. Chapter 2. CNF encodings. In Frontiers in Artificial Intelligence and Applications, Frontiers in artificial intelligence and applications. IOS Press, February 2021

    work page 2021

  29. [29]

    Romero, Alejandro Gomez Cadavid, Pavle Nikaˇcevi´c, Enrique Solano, Narendra N

    Sebasti´an V . Romero, Alejandro Gomez Cadavid, Pavle Nikaˇcevi´c, Enrique Solano, Narendra N. Hegade, Miguel Angel Lopez-Ruiz, Claudio Girotto, Masako Yamada, Panagiotis Kl. Barkoutsos, Ananth Kaushik, and Martin Roetteler. Protein folding with an all-to-all trapped-ion quantum computer, 2025

    work page 2025

  30. [30]

    Towards Hamiltonian Simulation with Decision Diagrams

    Aaron Sander, Lukas Burgholzer, and Robert Wille. Towards Hamiltonian Simulation with Decision Diagrams. In 2023 International Conference on Quantum Computing and Engineering, 5 2023

    work page 2023

  31. [31]

    Tian Sang, Paul Beame, and Henry A. Kautz. Heuristics for fast exact model counting. InInternational Conference on Theory and Applications of Satisfiability Testing, 2005

    work page 2005

  32. [32]

    The density-matrix renormalization group in the age of matrix product states

    Ulrich Schollw”ock. The density-matrix renormalization group in the age of matrix product states. Annals of Physics, 326(1):96–192, 2011

    work page 2011

  33. [33]

    Selinger.A Survey of Graphical Languages for Monoidal Categories, pages 289–355

    P . Selinger.A Survey of Graphical Languages for Monoidal Categories, pages 289–355. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. 43

    work page 2011

  34. [34]

    Ganak: A scalable probabilistic exact model counter

    Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S Meel. Ganak: A scalable probabilistic exact model counter. In IJCAI, volume 19, pages 1169–1176, 2019

    work page 2019

  35. [35]

    Masuo Suzuki. Relationship between d-dimensional quantal spin systems and (d+1)-dimensional ising systems: Equivalence, critical exponents and systematic approximants of the partition function and spin correlations. Progress of Theoretical Physics, 56(5):1454–1469, 11 1976

    work page 1976

  36. [36]

    Proposal of a compact and efficient sat encoding using a numeral system of any base

    Tomoya Tanjo, Naoyuki Tamura, and Mutsunori Banbara. Proposal of a compact and efficient sat encoding using a numeral system of any base. 2011

    work page 2011

  37. [37]

    The complexity of computing the permanent

    Leslie G Valiant. The complexity of computing the permanent. Theoretical computer science, 8(2):189– 201, 1979

    work page 1979

  38. [38]

    Hybrid quantum optimization in the context of minimizing traffic congestion, 2025

    Jedwin Villanueva, Gary J Mooney, Bhaskar Roy Bardhan, Joydip Ghosh, Charles D Hill, and Lloyd C L Hollenberg. Hybrid quantum optimization in the context of minimizing traffic congestion, 2025

    work page 2025

  39. [39]

    Enriching diagrams with algebraic operations

    Alejandro Villoria, Henning Basold, and Alfons Laarman. Enriching diagrams with algebraic operations. In International Conference on Foundations of Software Science and Computation Structures, pages 121–143. Springer, 2024

    work page 2024

  40. [40]

    Automating equational proofs in dirac notation

    Yingte Xu, Gilles Barthe, and Li Zhou. Automating equational proofs in dirac notation. Proc. ACM Program. Lang., 9(POPL), January 2025

    work page 2025

  41. [41]

    D-hammer: Efficient equational reasoning for labelled dirac notation, 2025

    Yingte Xu, Li Zhou, and Gilles Barthe. D-hammer: Efficient equational reasoning for labelled dirac notation, 2025

    work page 2025

  42. [42]

    Reducing quantum circuit synthesis to #SAT

    Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, and Alfons Laarman. Reducing quantum circuit synthesis to #SAT. In 31th International Conference on Principles and Practice of Constraint Programming (CP 2025),

    work page 2025

  43. [43]

    Accepted for publication. 44

    work page