Tuning Local Search for Satisfiability Testing

No. 1: Agents, AI in Art and Entertainment, Knowledge Representation, and Learning

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 13

Stochastic Search

Local search algorithms, particularly GSAT and WSAT, have attracted considerable recent attention, primarily because they are the best known approaches to several hard classes of satisfiability problems. However, replicating reported results has been difficult because the setting of certain key parameters is something of an art, and because details of the algorithms, not discussed in the published papers, can have a large impact on performance. In this paper we present an efficient probabilistic method for finding the optimal setting for a critical local search parameter, Maxflips, and discuss important details of two differing versions of WSAT. We then apply the optimization method to study performance of WSAT on satisfiable instances of Random 3SAT at the crossover point and present extensive experimental results over a wide range of problem sizes. We find that the results are well described by having the optimal value of Maxflips scale as a simple power of the number of variables, n, and the average run time scale sub-exponentially (basically as n^log(n)) over the range n = 25, . . . ,400.