Fast Sampling and Counting k-SAT Solutions in the Local Lemma Regime

Weiming Feng; Heng Guo; Yitong Yin; Chihao Zhang

doi:10.1145/3357713.3384255

Fast Sampling and Counting k-SAT Solutions in the Local Lemma Regime

Weiming Feng, Heng Guo, Yitong Yin, Chihao Zhang

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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 < n^o(1) and k ≥ 20logk + 20logd + 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 language	English
Title of host publication	Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing (STOC 2020)
Publisher	ACM
Pages	854-867
Number of pages	14
ISBN (Electronic)	9781450369794
DOIs	https://doi.org/10.1145/3357713.3384255
Publication status	Published - 22 Jun 2020
Event	52nd Annual ACM Symposium on Theory of Computing - Virtual conference, United States Duration: 22 Jun 2020 → 26 Jun 2020 http://acm-stoc.org/stoc2020/

Conference

Conference	52nd Annual ACM Symposium on Theory of Computing
Abbreviated title	STOC 2020
Country/Territory	United States
City	Virtual conference
Period	22/06/20 → 26/06/20
Internet address	http://acm-stoc.org/stoc2020/

Keywords / Materials (for Non-textual outputs)

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

Access to Document

10.1145/3357713.3384255Licence: All Rights Reserved

https://dl.acm.org/doi/10.1145/3357713.3384255Licence: All Rights Reserved

Cite this

@inproceedings{3bb0379a150c49a4835ad595858d19de,

title = "Fast Sampling and Counting k-SAT Solutions in the Local Lemma Regime",

abstract = "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 ≥ 20logk + 20logd + 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{\'a}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).",

keywords = "Markov chain Monte Carlo, Lov{\'a}sz local lemma, k-SAT, approximate counting",

author = "Weiming Feng and Heng Guo and Yitong Yin and Chihao Zhang",

year = "2020",

month = jun,

day = "22",

doi = "10.1145/3357713.3384255",

language = "English",

pages = "854--867",

booktitle = "Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing (STOC 2020)",

publisher = "ACM",

note = "52nd Annual ACM Symposium on Theory of Computing, STOC 2020 ; Conference date: 22-06-2020 Through 26-06-2020",

url = "http://acm-stoc.org/stoc2020/",

}

TY - GEN

T1 - Fast Sampling and Counting k-SAT Solutions in the Local Lemma Regime

AU - Feng, Weiming

AU - Guo, Heng

AU - Yin, Yitong

AU - Zhang, Chihao

PY - 2020/6/22

Y1 - 2020/6/22

N2 - 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 ≥ 20logk + 20logd + 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).

AB - 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 ≥ 20logk + 20logd + 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).

KW - Markov chain Monte Carlo

KW - Lovász local lemma

KW - k-SAT

KW - approximate counting

U2 - 10.1145/3357713.3384255

DO - 10.1145/3357713.3384255

M3 - Conference contribution

SP - 854

EP - 867

BT - Proceedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing (STOC 2020)

PB - ACM

T2 - 52nd Annual ACM Symposium on Theory of Computing

Y2 - 22 June 2020 through 26 June 2020

ER -

Fast Sampling and Counting k-SAT Solutions in the Local Lemma Regime

Abstract

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this