Belief propagation guided decimation fails on random formulas

Abstract

Let φ be a uniformly distributed random k-SAT formula with n variables and m clauses. Nonconstructive arguments show that φ is satisfiable for clause/variable ratios m/n ≤ rkSAT∼ 2k ln 2 with high probability. Yet no efficient algorithm is known to find a satisfying assignment beyond m/n ∼ 2k ln(k)/k with a nonvanishing probability. On the basis of deep but nonrigorous statistical mechanics ideas, a message passing algorithm called Belief Propagation Guided Decimation has been put forward (Mézard, Parisi, Zecchina: Science 2002; Braunstein, Mézard, Zecchina: Random Struc. Algorithm 2005). Experiments suggested that the algorithm might succeed for densities very close to rk-SAT for k = 3, 4, 5 (Kroc, Sabharwal, Selman: SAC 2009). Furnishing the first rigorous analysis of this algorithm on a nontrivial input distribution, in the present article we show that Belief Propagation Guided Decimation fails to solve random k-SAT formulas already for m/n = O(2k/k), almost a factor of k below the satisfiability threshold rk-SAT. Indeed, the proof refutes a key hypothesis on which Belief Propagation Guided Decimation hinges for such m/n. 2017 Copyright is held by the owner/author(s).ACM.