论文标题
稀疏散布可扩展的近似模型计数：理论和实践
Sparse Hashing for Scalable Approximate Model Counting: Theory and Practice
论文作者
论文摘要
给定N变量上的CNF公式F，模型计数或#SAT的问题是计算F的满足分配数。模型计数是具有多种应用的计算机科学中的一个基本问题。近年来，人们努力开发有效的算法技术，这些技术将古典的2-宇宙哈希助理与过去十年中SAT解决方面的显着进步相结合。这些技术通过随机XOR约束增强CNF公式F，并在所得的CNF-XOR公式上反复调用NP Oracle。实际上，对NP Oracle调用的呼叫被替换为SAT求解器，其运行时性能受到XOR约束大小的不利影响。 2-宇宙哈希功能的标准构造选择了每个变量，概率为p = 1/2，导致XOR限制在预期中的尺寸N/2。因此，挑战是设计稀疏的哈希功能，其中可以以较小的概率选择变量并导致较小尺寸的XOR约束。 在本文中，我们从理论和实践的角度解决了这一挑战。首先，我们将普遍哈希的放松形式化，称为浓缩哈希，并在这些哈希函数的浓度度量和布尔超振管的等二仪不平等之间建立了新颖而美丽的联系。这使我们能够在方差和色散索引上获得（log M）紧密的界限，并证明P = O（log（m）/m）足以设计从{0，1}^n到{0，1}^m的稀疏哈希函数的设计。然后，我们使用属于该集中哈希家族的稀疏哈希功能来开发新的近似计数算法。对我们在1893年的基准上对我们的算法进行全面的实验评估表明，稀疏哈希功能的使用可能会导致显着的加速。
Given a CNF formula F on n variables, the problem of model counting or #SAT is to compute the number of satisfying assignments of F . Model counting is a fundamental but hard problem in computer science with varied applications. Recent years have witnessed a surge of effort towards developing efficient algorithmic techniques that combine the classical 2-universal hashing with the remarkable progress in SAT solving over the past decade. These techniques augment the CNF formula F with random XOR constraints and invoke an NP oracle repeatedly on the resultant CNF-XOR formulas. In practice, calls to the NP oracle calls are replaced a SAT solver whose runtime performance is adversely affected by size of XOR constraints. The standard construction of 2-universal hash functions chooses every variable with probability p = 1/2 leading to XOR constraints of size n/2 in expectation. Consequently, the challenge is to design sparse hash functions where variables can be chosen with smaller probability and lead to smaller sized XOR constraints. In this paper, we address this challenge from theoretical and practical perspectives. First, we formalize a relaxation of universal hashing, called concentrated hashing and establish a novel and beautiful connection between concentration measures of these hash functions and isoperimetric inequalities on boolean hypercubes. This allows us to obtain (log m) tight bounds on variance and dispersion index and show that p = O( log(m)/m ) suffices for design of sparse hash functions from {0, 1}^n to {0, 1}^m. We then use sparse hash functions belonging to this concentrated hash family to develop new approximate counting algorithms. A comprehensive experimental evaluation of our algorithm on 1893 benchmarks demonstrates that usage of sparse hash functions can lead to significant speedups.
