论文标题
快速收敛任何时间型号计数
Fast Converging Anytime Model Counting
论文作者
论文摘要
模型计数是一个基本问题，从人工智能到正式验证，在许多应用中都具有影响力。由于模型计数的固有硬度，已经开发了近似技术来求解模型计数的现实世界实例。本文设计了一种新的方法，称为partialkc进行近似模型计数。这个想法是部分知识汇编的一种形式，可以提供对模型计数的无偏估计，该估计可以收敛到确切的计数。我们的经验分析表明，PartialKC在先前最新的近似计数器（包括SATS和ST）上实现了显着的可扩展性和准确性。有趣的是，经验结果表明，PartialKC在许多情况下达到了融合，因此提供了与最先进的确切计数相当的确切模型计数性能。
Model counting is a fundamental problem which has been influential in many applications, from artificial intelligence to formal verification. Due to the intrinsic hardness of model counting, approximate techniques have been developed to solve real-world instances of model counting. This paper designs a new anytime approach called PartialKC for approximate model counting. The idea is a form of partial knowledge compilation to provide an unbiased estimate of the model count which can converge to the exact count. Our empirical analysis demonstrates that PartialKC achieves significant scalability and accuracy over prior state-of-the-art approximate counters, including satss and STS. Interestingly, the empirical results show that PartialKC reaches convergence for many instances and therefore provides exact model counting performance comparable to state-of-the-art exact counters.
