Given a Boolean formula $\phi$ over $n$ variables, the problem of model counting is to compute the number of solutions of $\phi$. Model counting is a fundamental problem in computer science with wide-ranging applications. Owing to the \#P-hardness of the problems, Stockmeyer initiated the study of the complexity of approximate counting. Stockmeyer showed that $\log n$ calls to an NP oracle are necessary and sufficient to achieve $(\varepsilon,\delta)$ guarantees. The hashing-based framework proposed by Stockmeyer has been very influential in designing practical counters over the past decade, wherein the SAT solver substitutes the NP oracle calls in practice. It is well known that an NP oracle does not fully capture the behavior of SAT solvers, as SAT solvers are also designed to provide satisfying assignments when a formula is satisfiable, without additional overhead. Accordingly, the notion of SAT oracle has been proposed to capture the behavior of SAT solver wherein given a Boolean formula, an SAT oracle returns a satisfying assignment if the formula is satisfiable or returns unsatisfiable otherwise. Since the practical state-of-the-art approximate counting techniques use SAT solvers, a natural question is whether an SAT oracle is more powerful than an NP oracle in the context of approximate model counting. The primary contribution of this work is to study the relative power of the NP oracle and SAT oracle in the context of approximate model counting. The previous techniques proposed in the context of an NP oracle are weak to provide strong bounds in the context of SAT oracle since, in contrast to an NP oracle that provides only one bit of information, a SAT oracle can provide $n$ bits of information. We therefore develop a new methodology to achieve the main result: a SAT oracle is no more powerful than an NP oracle in the context of approximate model counting.

翻译：给定一个包含 $n$ 个变量的布尔公式 $\phi$，模型计数问题旨在计算 $\phi$ 的解的数量。模型计数是计算机科学中的一个基本问题，具有广泛的应用。由于该问题的 #P-难特性，Stockmeyer 开创了近似计数复杂性的研究。Stockmeyer 表明，对 NP 神谕进行 $\log n$ 次调用是实现 $(\varepsilon,\delta)$ 保证的充要条件。Stockmeyer 提出的基于哈希的框架在过去十年中对设计实用计数器产生了深远影响，其中 SAT 求解器在实际中替代了 NP 神谕调用。众所周知，NP 神谕无法完全捕捉 SAT 求解器的行为，因为 SAT 求解器还被设计为在公式可满足时，无需额外开销即可提供满足赋值。因此，SAT 神谕的概念被提出以捕捉 SAT 求解器的行为：给定一个布尔公式，若公式可满足则返回一个满足赋值，否则返回不可满足。由于实际中最先进的近似计数技术使用 SAT 求解器，一个自然的问题是：在近似模型计数的背景下，SAT 神谕是否比 NP 神谕更强大？本文的主要贡献在于研究 NP 神谕与 SAT 神谕在近似模型计数中的相对能力。先前在 NP 神谕背景下提出的技术难以在 SAT 神谕背景下提供强界，因为与仅提供一比特信息的 NP 神谕不同，SAT 神谕可提供 $n$ 比特信息。因此，我们开发了一种新方法以得出主要结论：在近似模型计数的背景下，SAT 神谕并不比 NP 神谕更强大。