Analysing Survey Propagation Guided Decimation on Random Formulas

Understand

Let $\varPhi$ be a uniformly distributed random $k$-SAT formula with $n$ variables and $m$ clauses.

• For clauses/variables ratio $m/n \leq r_{k\text{-SAT}} \sim 2^k\ln2$ the formula $\varPhi$ is satisfiable with high probability.
• However, no efficient algorithm is known to provably find a satisfying assignment beyond $m/n \sim 2k \ln(k)/k$ with a non-vanishing probability.
• Non-rigorous statistical mechanics work on $k$-CNF led to the development of a new efficient "message passing algorithm" called \emph{Survey Propagation Guided Decimation} [M\'ezard et al., Science 2002].