一句话:提出基于3-独立哈希的SAT解几乎均匀生成算法,在562个基准上全部成功而JVV超时544个。
给定布尔公式 φ 和分布参数 ε,几乎均匀生成要求随机生成器输出每个解的概率与 1/|sol(φ)| 相差不超过 (1+ε) 倍。此前 Jerrum、Valiant 和 Vazirani 的方案通过 SAT oracle 并采用 2-独立哈希函数实现。本文设计了一种新的随机算法,仍调用 SAT oracle,但改用 3-独立哈希函数。由于常用的 tabulation hashing 本身即为 3-独立,实际实现不会带来额外开销。作者在 562 个基准上评估:JVV 在 544 个实例上超时,而本文方案能处理全部 562 个实例。据作者所知,这是首个能处理实际应用实例的几乎均匀生成方案,并进一步分析了 SAT 查询大小与查询次数。
Given a Boolean formula φ and a distribution parameter ε, the problem of almost-uniform generation seeks to design a randomized generator such that every solution of φ is output with probability within (1 + ε)-factor of where sol(φ) is the set of all the solutions of φ. The prior state of the art scheme due to Jerrum, Valiant, and Vazirani, makes calls to a SAT oracle and employs 2 − wise independent hash functions. In this work, we design a new randomized algorithm that makes calls to a SAT oracle and employs 3 − wise independent hash functions. The widely used 2 − wise independent hashing is tabulation hashing proposed by Carter and Wegman. Since this classical scheme is also 3 − wise independent, we observe that practical implementation of our technique does not incur additional overhead. We demonstrate that theoretical improvements translate to practice; in particular, we conduct a comprehensive study over 562 benchmarks and demonstrate that while JVV would time out for 544 out of 562 instances, our proposed scheme can handle all the 562 instances. To the best of our knowledge, this is the first almost-uniform generation scheme that can handle practical instances from real-world applications. We also present a nuanced analysis focusing on the both the size of SAT queries as well as the number of queries.