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

Weiming Feng, Heng Guo, Yitong Yin, Chihao Zhang

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

We give new algorithms based on Markov chains to sample and approximately count satisfying assignments to k-uniform CNF formulas where each variable appears at most d times. For any k and d satisfying kd < no(1) and k ≥ 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 if k = ω(1) or d = ω(1)
Original languageEnglish
Article number40
Number of pages42
JournalJournal of the ACM
Volume68
Issue number6
Early online date5 Oct 2021
DOIs
Publication statusPublished - 1 Dec 2021

Keywords / Materials (for Non-textual outputs)

  • Markov chain Monte Carlo
  • Lovász local lemma
  • 𝑘-SAT
  • approximate counting

Fingerprint

Dive into the research topics of 'Fast sampling and counting k-SAT solutions in the local lemma regime'. Together they form a unique fingerprint.

Cite this