Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, developing algorithms for approximate counting is an important research area. Building on the practical success of SAT-solvers, the focus has recently shifted from theory to practical implementations of approximate counting algorithms. This has brought to focus new challenges, such as the design of auditable approximate counters that not only provide an approximation of the model count, but also a certificate that a verifier with limited computational power can use to check if the count is indeed within the promised bounds of approximation. Towards generating certificates, we start by examining the best-known deterministic approximate counting algorithm that uses polynomially many calls to a $\Sigma_2^P$ oracle. We show that this can be audited via a $\Sigma_2^P$ oracle with the query constructed over $n^2 \log^2 n$ variables, where the original formula has $n$ variables. Since $n$ is often large, we ask if the count of variables in the certificate can be reduced -- a crucial question for potential implementation. We show that this is indeed possible with a tradeoff in the counting algorithm's complexity. Specifically, we develop new deterministic approximate counting algorithms that invoke a $\Sigma_3^P$ oracle, but can be certified using a $\Sigma_2^P$ oracle using certificates on far fewer variables: our final algorithm uses only $n \log n$ variables. Our study demonstrates that one can simplify auditing significantly if we allow the counting algorithm to access a slightly more powerful oracle. This shows for the first time how audit complexity can be traded for complexity of approximate counting.

翻译：模型计数，即计算布尔公式的满足赋值数量，是一个具有广泛应用的 fundamental 问题。鉴于该问题的#P难度，开发近似计数算法是重要的研究方向。基于SAT求解器的实际成功，近年来研究焦点已从理论转向近似计数算法的实际实现。这带来了新的挑战，例如设计可审计的近似计数器——不仅提供模型计数的近似值，还需提供证书，使计算能力有限的验证者能够检查计数结果是否确实符合预期的近似范围。为生成证书，我们首先研究使用多项式次$\Sigma_2^P$预言机查询的最优已知确定性近似计数算法。我们证明该算法可通过$\Sigma_2^P$预言机进行审计，其查询构造涉及$n^2 \log^2 n$个变量，其中原始公式包含$n$个变量。由于$n$通常很大，我们提出能否减少证书中的变量数量——这是实现应用中至关重要的课题。我们证明这一目标可以实现，但需在计数算法复杂度上作出权衡。具体而言，我们开发了新的确定性近似计数算法：该算法调用$\Sigma_3^P$预言机，但可通过使用更少变量的证书由$\Sigma_2^P$预言机进行验证——最终算法仅需$n \log n$个变量。研究表明，若允许计数算法访问更强一阶的预言机，可显著简化审计过程。这首次展示了审计复杂度与近似计数复杂度之间的可交换性。