标题： 使用加权模型计数的量子物理 显示英文标题

标题： Quantum Physics using Weighted Model Counting

摘要： 加权模型计数（WMC）已被证明在计算机科学、物理学等领域的一系列任务中非常有效。 然而，现有的在量子物理中使用WMC的方法仅针对特定问题实例，缺乏一种通用框架来使用WMC表达问题。 这限制了这些方法在其他应用中的可重用性，并可能导致每个实例的数学严谨性不足。 我们提出了一种将线性代数问题（特别是物理学和量子计算中的问题）表达为WMC实例的方法。 我们通过引入一种将狄拉克符号转换为WMC问题的框架来实现这一点。 我们通过类型系统和语义学理论构建了这个框架，并在Python中提供了实现。 我们展示了我们的框架在计算几个物理模型的分区函数中的有效性：横场伊辛模型（量子）和庞茨模型（经典）。 结果表明，通过我们的框架，自动化推理中开发的启发式方法可以系统地应用于量子物理中的广泛问题类别。 显示英文摘要

摘要： 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.