Improving WalkSAT for random κ-satisfiability problem with κ > 3

Abstract

Stochastic local search (SLS) algorithms are well known for their ability to efficiently find models of random instances of the Boolean satisfiablity (SAT) problem. One of the most famous SLS algorithms for SAT is WalkSAT, which is an initial algorithm that has wide influence among modern SLS algorithms. Recently, there has been increasing interest in WalkSAT, due to the discovery of its great power on large random 3-SAT instances. However, the performance of WalkSAT on random k-SAT instances with κ > 3 lags far behind. Indeed, there have been few works in improving SLS algorithms for such instances. This work takes a large step towards this direction. We propose a novel concept namely multilevel make. Based on this concept, we design a scoring function called linear make, which is utilized to break ties in WalkSAT, leading to a new algorithm called WalkSATlm. Our experimental results on random 5- SAT and 7-SAT instances show that WalkSATlm improves WalkSAT by orders of magnitudes. Moreover, WalkSATlm significantly outperforms state-of-the-art SLS solvers on random 5-SAT instances, while competes well on random 7-SAT ones. Additionally, WalkSATlm performs very well on random instances from SAT Challenge 2012, indicating its robustness. Copyright © 2013, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.