Quantum Physics using Weighted Model Counting

TL;DR

This paper introduces a general framework converting linear algebraic problems in quantum physics into weighted model counting problems, enabling broader application and systematic analysis.

Contribution

It presents a theoretical and practical framework converting Dirac notation to WMC, with an implementation in Python for quantum and classical models.

Findings

Successfully applied to compute partition functions of quantum and classical models

Framework demonstrates potential for systematic application of automated reasoning heuristics

Enhances reusability and mathematical rigor in applying WMC to physics problems

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.

Equations

$$\mathrm{WMC}(\varphi ,W)=\sum _{\tau \models \varphi }W(\tau ),$$

$$\varphi \equiv \underset{i=1}{\overset{n}{\bigwedge }}\underset{j=1}{\overset{m}{\bigvee }}{x}_{ij},$$

$$\mathrm{WMC}(\varphi ,W)=\sum _{\tau :V\to \mathbb{B}}\varphi [\tau ]\prod _{v\in V}W(v,\tau (v)).$$

$$A\otimes B=\left[\begin{array}{ccc}{A}_{0,0}B& \cdots & A_{0,r-1}B\\ ⋮& \ddots & ⋮\\ A_{c-1,0}B& \cdots & A_{c-1,r-1}B\end{array}\right],(A_1\otimes B_1)(A_2\otimes B_2)=A_1{A}_2\otimes B_1{B}_2.$$

$$X=\left[\begin{array}{cc}0& 1\\ 1& 0\end{array}\right],Y=\left[\begin{array}{cc}0& -i\\ i& 0\end{array}\right],Z=\left[\begin{array}{cc}1& 0\\ 0& -1\end{array}\right],H=\frac{1}{\sqrt{2}}\left[\begin{array}{cc}1& 1\\ 1& -1\end{array}\right].$$

$$T::=\mathcal{S}\mid \mathcal{M}(q,m\to n)$$

$$e$$

$$s$$

$$M$$

$$\mid s\cdot M\mid \mathsf{trans}(M)\mid \mathsf{apply}(f,M)$$

Full text

1. 1 Introduction

2. 2 Preliminaries

3. 2.1 Boolean logic and weighted model counting

4. 2.2 Quantum notation

5. 3 Matrix Computations using WMC

6. 3.1 Code examples

7. 3.2 Language Syntax

8. 3.3 Type system

9. 3.3.1 Scalar type rules

1 Introduction

Problems in Quantum Physics

Quantum physics describes the behavior of fundamental particles, atoms, and molecules. Quantum computing promises breakthroughs in areas such as drug development, traffic optimization, and artificial intelligence [Romero2025, Villanueva2025, Li2022]. However, large-scale quantum hardware remains scarce and error-prone, making classical simulation of quantum systems essential for validating algorithms, studying physical models, and benchmarking quantum devices. Yet classical simulation is inherently challenging due to the exponential growth of the solution space. A central example is computing partition functions, which needs to sum over all possible configurations of a system and is crucial for understanding thermodynamic properties. Direct computation quickly becomes intractable as system size grows.

The Potential of Weighted Model Counting

One promising classical technique to compute partition functions is weighted model counting (WMC). Weighted model counting computes the total weight of all satisfying assignments to a weighted Boolean formula. Importantly, this framework extends to quantum physics: partition functions of quantum systems, such as the transverse-field Ising model, can be encoded as WMC instances, enabling classical solvers to directly tackle quantum problems. We write:

[TABLE]

where $W$ assigns weights to assignments $\tau$ satisfying the Boolean formula $\phi$. This task is #$\mathsf{P}$-hard [valiant1979complexity, Hunt1989], yet modern solvers based on clause learning, algebraic decision diagrams, or tensor networks can handle large instances [Sang2005, Sharma2019, Dudek2020, Dudek2021, Dudek2021ProCount]. Initial applications include probabilistic reasoning [Dilkas2021, Chavira2008, Paredes2019].

These advances in clause learning and tensor network methods have enabled WMC applications in statistical physics and quantum computing: Mei et al. [Mei2024b, Mei2024c, Mei2024] demonstrated that WMC can simulate quantum circuits by reducing gate operations to Boolean formulas. Even complex-valued simulations can be reduced to real or Boolean WMC instances. In parallel, Nagy et al. [Nagy2024] showed that the Ising model partition function can be reduced to the WMC problem, and that tensor-based WMC solvers outperform traditional physics tools like CATN [Pan2020].

Contributions

This paper makes the following contributions:

A general encoding framework for $q^{n}\times q^{m}$ matrices using WMC, supporting operations such as addition, multiplication, and computing the trace. We define a formal language for encoding Dirac notation and prove correctness of the encoding. 2. 2.

A Python implementation, DiracWMC, available at [DiracWMC], used to generate the experiments in Section LABEL:sec:ising, LABEL:sec:quantumising, and LABEL:sec:potts. 3. 3.

Applications to the partition function of the transverse-field Ising model (quantum) and the Potts model (classical), demonstrating WMC beyond previously explored domains.

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.

Overview

The matrices arising in partition function computations decompose as tensor products of small local operators, yielding matrices that are exponentially large but highly sparse. Direct matrix computation fails to exploit this sparsity; our approach instead encodes matrix entries as weighted Boolean formulas and reduces linear algebra to WMC, which is specifically designed to handle such structure efficiently. We define a formal language for Dirac notation, prove correctness of the encoding (Section 3), and implement the framework as DiracWMC. We demonstrate the approach on three models: the classical Ising model (Section LABEL:sec:ising), the transverse-field Ising model (Section LABEL:sec:quantumising), and the Potts model (Section LABEL:sec:potts), with experimental comparisons against TensorOrderincluded throughout. Preliminary definitions from Boolean logic, weighted model counting, and Dirac notation are collected in Section 2. We conclude in Section LABEL:sec:conclusion.

2 Preliminaries

This section fixes notation used throughout. Unless stated otherwise, $\mathbb{B}=\{0,1\}$ and all matrices are over a field $\mathbb{F}$ (typically $\mathbb{R}$ or $\mathbb{C}$).

2.1 Boolean logic and weighted model counting

Let $V$ be a finite set of Boolean variables, $\tau:V\to\mathbb{B}$ an assignment, and $\phi$ a Boolean formula over $V$. We write $\phi[\tau]\in\mathbb{B}$ for its truth value under $\tau$. For $v\in V$, we define literals $v$ and $\overline{v}$ (the negation $\neg v$ of $v$). A formula is in conjunctive normal form (CNF) if

[TABLE]

with each $x_{ij}$ a literal. All instances in our experiments are supplied to counters in CNF.

To assign weights to formulas, we use a weight function on assignments as introduced in Section 1. To enable powerful heuristics [Chavira2008], the weight function is limited to literals as Definition 1 shows.

Definition 1** (Weighted model counting).**

Let $W:V\times\mathbb{B}\to\mathbb{F}$ be a function called the weight function. The weighted model count of $\phi$ w.r.t. $W$ is

[TABLE]

We use $\mathrm{dom}(W)=V$, and abbreviate $W(v)=W(v,1)$ and $W(\overline{v})=W(v,0)$.

2.2 Quantum notation

We adopt standard Dirac notation and Kronecker algebra for $q^{n}\times q^{m}$ matrices.

Bras, kets, and matrix elements

Moreover, we denote by $\bra{i}_{q}$ (row) and $\ket{i}_{q}$ (column) the computational basis vectors with a $1$ at position $i$ (zero-based) and [math] elsewhere. For a matrix $M$, $\bra{j}M\ket{i}=M_{ij}$.

Kronecker product

For matrices $A,B$, their Kronecker or tensor product is given by

[TABLE]

Trace

$\mathrm{tr}(M)$ denotes the matrix trace; $\mathrm{tr}(A\otimes B)=\mathrm{tr}(A)\mathrm{tr}(B)$.

Single-qubit gates

As usual, we let

[TABLE]

All are involutions; we will use $X=HZH$ in Sec. LABEL:sec:quantumising.

Matrix exponential

For a square matrix $M$, $\exp(M)=\sum_{k\geq 0}M^{k}/k!$; if $M$ is diagonal, $\exp(M)$ is the diagonal of entrywise exponentials. For large non-diagonal $M$ we use standard scaling–and–squaring with Padé approximants [Al-Mohy2010].

3 Matrix Computations using WMC

Here, we introduce weighted model counting (WMC) representations of general matrices. A WMC representation of quantum circuits was previously given in [Mei2024, Mei2024b, Mei2024c]. We aim to generalize and formalize this work by allowing an arbitrary base dimension of subspaces $q$ (qudits). We also add support for any $q^{n}\times q^{m}$ matrix, instead of just row/column vectors and square matrices.

We represent matrices as tuples $(\phi,W,x,y,q)$ of a Boolean formula, weight function, input and output variables, and some base size, respectively. The formula and weight function form the basis of model counting instances, used for every entry in the matrix. The input/output variables act as pointers to the specific entries in the matrix, which are obtained by adding restrictions to the values of these variables to the formula $\phi$. Scalars are represented by WMC instances $(\phi,W)$, where the value of the scalar is $\mathrm{WMC}(\phi,W)$.

We also provide encodings for several common matrix operations that can be performed on these representations directly, such as matrix multiplication, taking the trace, and computing the Kronecker product. To formalize the operations and prove their correctness, we first introduce a language of scalars and matrices, built from scalar constants, bras, and kets. This language is similar to D-Hammer, introduced by Xu et al. [Xu2025]. However, the language we introduce in this work is much simpler and neither supports contexts nor labeled matrices.

We introduce two kinds of denotational semantics on this language: $\llbracket\cdot\rrbracket_{v}$ returns the actual matrix or scalar that an expression represents. In contrast, $\llbracket\cdot\rrbracket_{r}$ returns an equivalence class of (matrix or scalar) representations that corresponds with the matrix or scalar.

Before we introduce this formal language, however, we give some code examples in our implementation of the language DiracWMC.

3.1 Code examples

The language is implemented using Python in the package DiracWMC [DiracWMC]. Full instructions on how to install and use the package are included there. Consider the following basic example, which calculates the product of a ket and a bra, and displays the result:

⬇

from wcnf_matrix import *

I = Index(2)

M = ket(I[0]) * bra(I[1])

print(value(M))

[ 0.0 1.0

0.0 0.0 ]

First, we import all of the contents of the DiracWMC package (called wcnf_matrix in the Python code). Then we create a space in which to perform operations, which we do using Index. The number $2$ indicates that we use $q=2$, i.e., we are working with qubits. The third line then creates two objects, a ket and a bra. These do not store the values of the two vectors explicitly, but rather store the tuples $(\phi,W,x,y,q)$ that can be used to calculate the entries in the matrices. In this example, we multiply the column vector $(1,0)^{T}$ with the row vector $(1,0)$. This then results in a new object, which again stores a tuple $(\phi,W,x,y,q)$ instead of the entries in the matrix. To get the actual entries of the matrix, we use value(M).

We can replace the index number $2$ with $3$ to get a $3\times 3$ matrix instead:

⬇

from wcnf_matrix import *

I = Index(3)

M = ket(I[0]) * bra(I[1])

print(value(M))

[ 0.0 1.0 0.0

0.0 0.0 0.0

0.0 0.0 0.0 ]

Matrices can be multiplied and added, and the Kronecker product of two matrices can be determined:

⬇

from wcnf_matrix import *

I = Index(3)

M1 = ket(I[0]) * bra(I[1])

M2 = ket(I[2]) * bra(I[0])

print(value(M1 * M2))

[ 0.0 0.0 0.0

0.0 0.0 0.0

0.0 0.0 0.0 ]

print(value(3.3 * M1 + M2))

[ 0.0 3.3 0.0

0.0 0.0 0.0

1.0 0.0 0.0 ]

print(value(M1 ** M2))

[ 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 1.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0

0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 0.0 ]

The true power of the package lies in cases where the explicit values of the matrix are not required. For example, the trace can be calculated using M.trace_formula(). This returns CNF and WeightFunction objects. The trace can be calculated by passing the CNF formula as an argument to a call to the WeightFunction object.

⬇

from wcnf_matrix import *

from functools import reduce

I = Index(2)

M1 = 2 * ket(I[0]) * bra(I[0]) + ket(I[1]) * bra(I[1])

print(value(M1))

[ 2.0 0.0

0.0 1.0 ]

M2 = reduce(lambda x, y: x ** y, [M1]*100)

cnf, weight_func = M2.trace_formula()

print(weight_func(cnf))

5.15378e+47

In this example, we use the Python built-in reduce to create an object M2 that represents a $2^{100}\times 2^{100}$ matrix. Then we calculate the trace of this large matrix using a model counter.

We could also retrieve entries in this matrix by multiplying it by bras and kets. In the following example, we calculate the top-left entry in the matrix:

⬇

... (continued) ...

B = reduce(lambda x, y: x ** y, [bra(I[0])]*100)

K = reduce(lambda x, y: x ** y, [ket(I[0])]*100)

print(value(B * M2 * K))

[ 1.26765e+30 ]

It is also possible to label the different dimensions of the matrix, such that matrices acting on different subspaces can be multiplied and added. In the following example, we apply a matrix M on a subspace labeled with r1 (using the syntax M | r1), while the vector we apply it to acts on subspaces r1 and r2. This example also shows the use of uset, which returns an iterable I[0], I[1], …, I[q-1].

⬇

from wcnf_matrix import *

from functools import reduce

I = Index(2)

r1, r2 = Reg(I), Reg(I)

phi = lambda index: reduce(lambda x, y: x + y, (ket(nv, nv) for nv in

... uset(index))) # Returns column vector (1, 1, 1, 1)^T

M = ket(I[0]) * bra(I[0]) # Matrix [(1, 0), (0, 0)]

print(value((M | r1) * (phi(I) | (r1, r2))))

[ 1.0

0.0

0.0

0.0 ] | (reg0, reg1)

Note that the resulting matrix is still labeled. To get a matrix M without labels, use M.mat.

By default, the package uses the DPMC model counter. However, it is possible to change this to Cachet or TensorOrder using the set_model_counter method. It is also possible to set the type of variable encoding used in the matrix representations, which may have a performance impact for $q>2$. Variable encodings are discussed in more detail later in this section and in Appendix LABEL:chapter:encodings.

⬇

from wcnf_matrix import *

set_model_counter(DPMC) # Default

set_model_counter(Cachet)

set_model_counter(TensorOrder)

set_var_rep_type(LogVarRep) # Default

set_var_rep_type(OrderVarRep)

set_var_rep_type(OneHotVarRep)

3.2 Language Syntax

The formal language we introduce has two types of expressions: scalars and matrices. Scalars from a field $\mathbb{F}$ are of type $\mathcal{S}$. Matrices have a type that contains the size of the matrix and its base size. A base size of $q\in\mathbb{Z}_{\geq 2}$ is used to represent $q^{n}\times q^{m}$ matrices. The intuition of this number is that it represents the dimension of the smallest vector space that all of our matrices act on. For a system of qubits, for example, a base size of $q=2$ would be used, since elementary operations on qubits are performed using $2\times 2$ unitary matrices. Any unitary acting on multiple qubits has dimensions that are a power of two.

We write the type of a matrix as $\mathcal{M}(q,m\to n)$, representing a $q^{n}\times q^{m}$ matrix, with $n,m\in\mathbb{Z}_{\geq 0}$. Note that $m$ and $n$ do not indicate the size of the matrix directly, but rather the number of “input and output subspaces”. Also note the reversal of the order of $n$ and $m$. We use this notation because a $q^{n}\times q^{m}$ matrix ($q^{n}$ rows and $q^{m}$ columns) is generally interpreted as a linear map $\mathbb{F}^{q^{m}}\to\mathbb{F}^{q^{n}}$.

More formally, for $n,m\in\mathbb{Z}_{\geq 0}$ and $q\in\mathbb{Z}_{\geq 2}$ the type syntax is

[TABLE]

The syntax of expressions $e$ is split up into scalars $s$ and matrices $M$.

[TABLE]

Here $\alpha\in\mathbb{F}$ is an arbitrary constant and $f:\mathbb{F}\to\mathbb{F}$ is an arbitrary field endomorphism.

Scalar expressions can be combined using multiplication and addition. Applying a field endomorphism to a scalar also results in another scalar. In addition, taking the trace or getting a specific entry from a matrix gives a scalar.

The most basic matrices are the bra and ket, which are expressions for length-$q$ row and column computational basis vectors, respectively. These vectors have zeros everywhere except at the entry with index $0\leq i<q$. Matrices can also be multiplied and added. In addition, we have syntax for taking the Kronecker product, matrix-scalar multiplication, and taking the transpose of a matrix. We also add support for applying a field endomorphism $f$ to every entry of the matrix.

3.3 Type system

The type system associates expressions with types. We say that the expression $e$ has type $T$ if $\vdash e:T$ can be proven using the type rules below.

3.3.1 Scalar type rules

The usual rules for scalars apply: Multiplying or adding two scalars results in a scalar, and applying a field endomorphism to a scalar yields a scalar as well. In addition, any element of $\mathbb{F}$ is a scalar.