局部引理 regime 下 k-SAT 解的快速采样与计数

我们给出基于马尔可夫链的新算法，用于采样并近似计数满足 $k$-一致 CNF 公式的赋值，其中每个变量至多出现 $d$ 次。对于任意满足 $kd<n^{o(1)}$ 且 $k\ge 20\log k + 20\log d + 60$ 的 $k$ 和 $d$，新采样算法在近线性时间内运行，计数算法在近二次时间内运行。我们的方法受 Moitra (JACM, 2019) 启发，其卓越地利用 Lov\'{a}sz 局部引理进行近似计数。我们的主要技术贡献是利用局部引理绕过传统马尔可夫链方法中的连通性障碍，使成熟的 MCMC 方法可应用于如 SAT 解这类不连通状态空间。我们方法的益处在于避免局部结构的枚举并获得固定的多项式运行时间，即便 $k=\omega(1)$ 或 $d=\omega(1)$。