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 ⩽ r k − SAT ∼ 2 k ln 2 with high probability. Yet no efficient algorithm is known to find a satisfying assignment beyond m / n ∼ 2 k 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 r k − 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 (2 k / k ), almost a factor of k below the satisfiability threshold r k − SAT . Indeed, the proof refutes a key hypothesis on which Belief Propagation Guided Decimation hinges for such m / n .