# 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.

## Key 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.