Message-passing and local heuristics as decimation strategies for satisfiability

摘要

Decimation is a simple process for solving constraint satisfaction problems, by repeatedly fixing variable values and simplifying without reconsidering earlier decisions. We investigate different decimation strategies, contrasting those based on local, syntactic information from those based on message passing, such as statistical physics based Survey Propagation (SP) and the related and more well-known Belief Propagation (BP). Our results reveal that once we resolve convergence issues, BP itself can solve fairly hard random k-SAT formulas through decimation; the gap between BP and SP narrows down quickly as k increases. We also investigate observable differences between BP/SP and other common CSP heuristics as decimation proceeds, exploring the hardness of the decimated formulas and identifying a somewhat unexpected feature of message passing heuristics, namely, unlike other heuristics for satisfiability, they avoid unit propagation as variables are fixed.