The Statistical Mechanics of k-Satisfaction
Scott Kirkpatrick, G. Györgyi, Naftali Tishby, Lidror Troyansky · 1993
The satisfiability of random CNF formulae with precisely k variables per clause ("k-SAT") is a popular testbed for the performance of search algorithms. Formulae have M clauses from N variables, randomly negated, keeping the ratio ff = M=N fixed. For k = 2, this model has been proven to have a sharp threshold at ff = 1 between formulae which are almost aways satisfiable and formulae which are almost never satisfiable as N ! 1. Computer experiments for k = 2, 3, 4, 5 and 6, (carried out in collaboration with B. Selman of ATT Bell Labs) show similar threshold behavior for each value of k. Finite-size scaling, a theory of the critical point phenomena used in statistical physics, is shown to characterize the size dependence near the threshold. Annealed and replica-based mean field theories give a good account of the results. Permanent address: IBM TJ Watson Research Center, Yorktown Heights, NY 10598 USA. ([email protected]) Portions of this work were done while visiting the...