Belief Propagation Guided Decimation Fails on Random Formulas.

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 ⩽ rk− SAT ∼ 2kln 2 with high probability. Yet no efficient algorithm is known to find a satisfying assignment beyond m/n ∼ 2kln (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.