Random walk algorithm (RWalkSAT) is one of the simplest and oldest heuristics for satisfiability problems. In contrast to many experimental results, relatively few rigorous analyses of RWalkSAT are available. Up to now, runtime results of small density random 3-SAT have been achieved showing RWalkSAT terminates successfully in linear time up to clause density 1.63. This paper presents a rigorous runtime analysis of RWalkSAT for 3-CNF formulas generated under the planted assignment distribution. It proves that with overwhelming probability, when starting from any initial assignment |x|< 0.9999n, the expected number of steps until RWalkSAT on random planted formulas with a large constant density finds the planted assignment (1, . . . ,1) is at least Ω(1.1514n) and at most O(n21.1517n).
展开▼