Improving stochastic local search for SAT with a new probability distribution

Abstract

This paper introduces a new SLS-solver for the satisfiability problem. It is based on the solver gNovelty+. In contrast to gNovelty+, when our solver reaches a local minimum, it computes a probability distribution on the variables from an unsatisfied clause. It then flips a variable picked according to this distribution. Compared with other state-of-the-art SLS-solvers this distribution needs neither noise nor a random walk to escape efficiently from cycles. We compared this algorithm which we called Sparrow to the winners of the SAT 2009 competition on a broad range of 3-SAT instances. Our results show that Sparrow is significantly outperforming all of its competitors on the random 3-SAT problem. © 2010 Springer-Verlag.