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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Disentangling the Gap Between Quantum and #SAT

  • Jingyi Mei,
  • Jan Martens,
  • Alfons Laarman

摘要

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.