Model counting of Disjunctive Normal Form (DNF) formulas is a critical problem in applications such as probabilistic inference and network reliability. For example, it is often used for query evaluation in probabilistic databases. Due to the computational intractability of exact DNF counting, there has been a line of research into a variety of approximation algorithms. These include Monte Carlo approaches such as the classical algorithms of Karp, Luby, and Madras (1989), as well as methods based on hashing (Soos et al. 2023), and heuristic approximations based on Neural Nets (Abboud, Ceylan, and Lukasiewicz 2020). We develop a new Monte Carlo approach with an adaptive stopping rule and short-circuit formula evaluation. We prove it achieves Probably Approximately Correct (PAC) learning bounds and is asymptotically more efficient than the previous methods. We also show experimentally that it out-performs prior algorithms by orders of magnitude, and can scale to much larger problems with millions of variables.

翻译：析取范式（DNF）公式的模型计数是概率推理和网络可靠性等应用中的关键问题，例如常用于概率数据库中的查询评估。由于精确DNF计数的计算难解性，学界已发展了一系列近似算法的研究。这些方法包括蒙特卡洛方法（如Karp、Luby和Madras于1989年提出的经典算法）、基于哈希的方法（Soos等人，2023年）以及基于神经网络的启发式近似（Abboud、Ceylan和Lukasiewicz，2020年）。我们提出了一种具有自适应停止规则和短路公式评估的新型蒙特卡洛方法。我们证明该方法满足概率近似正确（PAC）学习界限，并且在渐近意义上比现有方法更高效。实验结果表明，该方法的性能较现有算法提升了数个数量级，能够扩展到包含数百万变量的大规模问题。