Can rare SAT formulas be easily recognized? On the efficiency of message passing algorithms for K-SAT at large clause-to-variable ratios

TL;DR

This paper explores the difficulty of recognizing rare satisfiable K-SAT formulas at large clause-to-variable ratios, showing they resemble planted instances and can be efficiently identified using message-passing algorithms.

Contribution

It demonstrates that rare satisfiable K-SAT instances at high ratios are similar to planted instances and can be efficiently recognized with message-passing algorithms.

Findings

Rare satisfiable instances resemble planted models

Message-passing algorithms can identify these instances efficiently

Recognition can be achieved in O(log N) time

Abstract

For large clause-to-variable ratio, typical K-SAT instances drawn from the uniform distribution have no solution. We argue, based on statistical mechanics calculations using the replica and cavity methods, that rare satisfiable instances from the uniform distribution are very similar to typical instances drawn from the so-called planted distribution, where instances are chosen uniformly between the ones that admit a given solution. It then follows, from a recent article by Feige, Mossel and Vilenchik, that these rare instances can be easily recognized (in O(log N) time and with probability close to 1) by a simple message-passing algorithm.