Disentangling the Gap Between Quantum and #SAT
摘要
Weighted model counting (#SAT) has recently been shown to deliver a promising new method for tackling core problems in quantum circuit analysis. However, the development of weighted model counting tools is currently strongly motivated by applications in the domain of probabilistic computing, where weights consist of positive probabilities. Quantum computing, on the other hand, deals with complex amplitudes, which include the negative domain and are subject to the \(\ell ^2\) norm, contrary to the \(\ell ^1\) norm used for probabilities. The current paper explores reductions from quantum circuit semantics to weighted model counting over the complex, real, natural and integer numbers (e.g., \(\#\text {SAT}_\mathbb {C}\) , \(\#\text {SAT}_\mathbb R\) , etc.), and various sub(semi)rings of those. This study thereby charts tradeoffs between counting over simpler algebras and the costs of the reduction. While previous works recommend the use of different (semi)rings, like those including negative numbers, we can now more precisely state the tradeoff introduced by this change as (polynomial) blowup of the length of the encoding as #SAT formula, the number of variables and the structure of the formula. Moreover, our final encoding to \(\#\text {SAT}_{\{0,1\}}\) (unweighted model counting) represents an exact solution, obviating the need for floating-point calculations that could potentially cause numerical instability.