可扩展的近似模型计数器
A Scalable Approximate Model Counter
摘要：
命题模型计数}（#SAT），即，计算命题公式的满足赋值的个数是一个具有重要理论意义和实际意义的问题。由于问题的内在复杂性，近似模型计数，它计数的数量满足指定的公差和置信水平内的分配，提出了作为一个实用的替代精确模型计数。然而，近似模型计数基本上只在理论上进行了研究。由于Karp和Luby，唯一报告的近似模型计数的实现仅适用于DNF公式。CNF公式的一些现有工具是边界模型计数器;它们可以处理实际的问题大小，但不能在给定的公差和置信度内提供计数，因此不是近似模型计数器。我们在这里提出了一种新的算法，以及一个参考实现，这是第一个可扩展的近似模型计数器CNF公式。该算法通过向SAT求解器发出多项式数量的调用来工作。我们的工具ApproxMC可扩展到包含数万个变量的公式。仔细的实验比较表明，ApproxMC报告，具有高置信度，边界接近精确的计数，也成功地报告边界与小公差和高置信度的情况下，太大的计算精确的模型计数。
英文摘要：
Propositional model counting} (#SAT), i.e., counting the number of satisfying assignments of a propositional formula, is a problem of significant theoretical and practical interest. Due to the inherent complexity of the problem, approximate model counting, which counts the number of satisfying assignments to within given tolerance and confidence level, was proposed as a practical alternative to exact model counting. Yet, approximate model counting has been studied essentially only theoretically. The only reported implementation of approximate model counting, due to Karp and Luby, worked only for DNF formulas. A few existing tools for CNF formulas are bounding model counters; they can handle realistic problem sizes, but fall short of providing counts within given tolerance and confidence, and, thus, are not approximate model counters. We present here a novel algorithm, as well as a reference implementation, that is the first scalable approximate model counter for CNF formulas. The algorithm works by issuing a polynomial number of calls to a SAT solver. Our tool, ApproxMC, scales to formulas with tens of thousands of variables. Careful experimental comparisons show that ApproxMC reports, with high confidence, bounds that are close to the exact count, and also succeeds in reporting bounds with small tolerance and high confidence in cases that are too large for computing exact model counts.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
