Quantum circuit compilation comprises many computationally hard reasoning tasks that nonetheless lie inside #$\mathbf{P}$ and its decision counterpart in $\mathbf{PP}$. The classical simulation of general quantum circuits is a core example. We show for the first time that a strong simulation of universal quantum circuits can be efficiently tackled through weighted model counting by providing a linear encoding of Clifford+T circuits. To achieve this, we exploit the stabilizer formalism by Knill, Gottesmann, and Aaronson and the fact that stabilizer states form a basis for density operators. With an open-source simulator implementation, we demonstrate empirically that model counting often outperforms state-of-the-art simulation techniques based on the ZX calculus and decision diagrams. Our work paves the way to apply the existing array of powerful classical reasoning tools to realize efficient quantum circuit compilation; one of the obstacles on the road towards quantum supremacy.

翻译：量子电路编译包含许多计算上困难的推理任务，这些任务仍属于#$\mathbf{P}$及其在$\mathbf{PP}$中的判定对应类。通用量子电路的经典模拟是一个核心示例。我们首次证明，通过为Clifford+T电路提供线性编码，通用量子电路的强模拟可以通过加权模型计数高效处理。为实现这一点，我们利用了Knill、Gottesmann和Aaronson的稳定子形式化方法，以及稳定子态构成密度算子基这一事实。通过开源模拟器实现，我们实证展示模型计数通常优于基于ZX演算和决策图的最先进模拟技术。我们的工作为应用现有强大的经典推理工具实现高效量子电路编译铺平了道路——这是通往量子霸权道路上的障碍之一。