Fast sampling and counting k-SAT solutions in the local lemma regime

Fast sampling and counting k-SAT solutions in the local lemma regime
复制标题

局部引理体系中的快速采样和计数 k-SAT 解决方案

DOI:
10.1145/3469832
复制
发表时间:
2021
期刊:
影响因子:
2.5
通讯作者:
Zhang Chihao
Zhang Chihao
中科院分区:
计算机科学2区
文献类型:
--
作者:
Feng Weiming;Guo Heng;Yin Yitong;Zhang Chihao

文献摘要

相似文献

本文给出了基于马尔可夫链的抽样和近似计数满足一致CNF公式的赋值的新算法,其中每个变量出现的次数最多。对于满足kd < no(1)且k ≥ 20 logk+ 20 logd+ 60的任意kandd,新的采样算法的运行时间接近线性时间,计数算法的运行时间接近二次时间。我们的方法受到Moitra(JACM,2019)的启发,该方法在近似计数中显著利用了Lovász局部引理。我们的主要技术贡献是使用本地引理绕过传统的马尔可夫链方法中的连接障碍,这使得发达的MCMC方法适用于断开状态空间,如SAT解决方案。我们的方法的好处是避免了局部结构的枚举,并获得固定的多项式运行时间,即使k = ω(1)或d = ω(1)。
We give new algorithms based on Markov chains to sample and approximately count satisfying assignments tok-uniform CNF formulas where each variable appears at mostdtimes. For anykanddsatisfyingkd< no(1)andk≥ 20 logk+ 20 logd+ 60, the new sampling algorithm runs in close to linear time, and the counting algorithm runs in close to quadratic time.Our approach is inspired by Moitra (JACM, 2019), which remarkably utilizes the Lovász local lemma in approximate counting. Our main technical contribution is to use the local lemma to bypass the connectivity barrier in traditional Markov chain approaches, which makes the well-developed MCMC method applicable on disconnected state spaces such as SAT solutions. The benefit of our approach is to avoid the enumeration of local structures and obtain fixed polynomial running times, even ifk= ω (1) or d = ω (1).