An efficient local search method for random 3-satisfiability

We report on some exceptionally good results in the solution of randomly generated 3-satisfiability instances using the “record-to-record travel (RRT)” local search method. When this simple, but less-studied algorithm is applied to random one-million variable instances from the problemʹs satisfiable phase, it seems to find satisfying truth assignments almost always in linear time, with the coefficient of linearity depending on the ratio α of clauses to variables in the generated instances. RRT has a parameter for tuning “greediness”. By lessening greediness, the linear time phase can be extended up to very close to the satisfiability threshold αc. Such linear time complexity is typical for random-walk based local search methods for small values of α. Previously, however, it has been suspected that these methods necessarily lose their time linearity far below the satisfiability threshold. The only previously introduced algorithm reported to have nearly linear time complexity also close to the satisfiability threshold is the survey propagation (SP) algorithm. However, SP is not a local search method and is more complicated to implement than RRT. Comparative experiments with the WalkSAT local search algorithm show behavior somewhat similar to RRT, but with the linear time phase not extending quite as close to the satisfiability threshold.