paperbot · PL 论文追踪

全部论文 待读 收藏

P2 On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing

SAT 解的几乎均匀生成:3-独立哈希的威力
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10 · 该论文属于 SAT/约束求解与随机生成算法,仅与形式化验证的底层求解器背景有间接关联;不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 7 inbox
Remi Delannoy, Kuldeep S. Meel
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出基于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 查询大小与查询次数。

问题
给定布尔公式 φ 和分布参数 ε,如何设计随机生成器,使每个解的输出概率与 1/|sol(φ)| 的偏差在 (1+ε) 倍以内,即几乎均匀生成 SAT 解。
方法
提出一种新的随机算法,使用 SAT oracle 并采用 3-独立哈希函数替代传统 2-独立哈希;利用 tabulation hashing 本身是 3-独立的特点,使实际实现不增加额外开销。
评估
在 562 个基准实例上与 JVV 方案对比,JVV 在 544 个实例上超时,而本文方案成功处理全部 562 个实例,并分析 SAT 查询大小与查询次数。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{DelannoyM22,
  title = {On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing},
  author = {Remi Delannoy and Kuldeep S. Meel},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533338}
}