Quantum physics using weighted model counting

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, which comprise of a formula with weighted variables. This approach preserves the structural and sparsity information of a problem, while giving access to efficient, general purpose model counting implementations. 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 automated reasoning heuristics, including clause learning, algebraic decision diagrams, and tensor network decomposition, can be systematically applied through a single unified framework to a wide class of quantum physics problems, including those requiring non-commuting operators, without problem-specific solver engineering. The framework naturally supports complex-valued weights through a reduction to real-valued WMC instances, broadening its applicability to a wider class of quantum models.