Improving WalkSAT for Random k-Satisfiability Problem with k > 3
Improving WalkSAT for Random k-Satisfiability Problem with k > 3
复制标题
DOI：
10.1609/aaai.v27i1.8554
复制
发表时间：
2013-06
期刊：
影响因子：
--
通讯作者：
Shaowei Cai;Kaile Su;Chuan Luo
中科院分区：
文献类型：
--
作者：
Shaowei Cai;Kaile Su;Chuan Luo
随机局部搜索（SLS）算法以其有效地找到布尔可满足性（SAT）问题的随机实例模型的能力而闻名。其中最著名的SAT SLS算法是WalkSAT，它是现代SLS算法中影响最广泛的一种初始算法。最近，由于在大型随机3-SAT实例上发现了强大的功能，人们对WalkSAT的兴趣越来越大。然而，WalkSAT在随机的$k$-SAT实例上的性能远远落后于$k bbb30 $。实际上，针对此类实例改进SLS算法的工作很少。这项工作朝着这个方向迈出了一大步。我们提出了一个新颖的概念，即多级$ $make$。基于这个概念，我们设计了一个叫做$linear$ $make$的评分函数，利用它来打破WalkSAT中的关系，从而产生了一个叫做WalkSAT$lm$的新算法。我们在随机5-SAT和7-SAT实例上的实验结果表明，WalkSAT$lm$提高了WalkSAT的数量级。此外，WalkSAT$lm$在随机5-SAT实例上明显优于最先进的SLS求解器，而在随机7-SAT实例上竞争良好。此外，WalkSAT$lm$在2012年SAT挑战赛的随机实例上表现非常好，表明其稳健性。
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 $k>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 WalkSAT$lm$. Our experimental results on random 5-SAT and 7-SAT instances show that WalkSAT$lm$ improves WalkSAT by orders of magnitudes. Moreover, WalkSAT$lm$ significantly outperforms state-of-the-art SLS solvers on random 5-SAT instances, while competes well on random 7-SAT ones. Additionally, WalkSAT$lm$ performs very well on random instances from SAT Challenge 2012, indicating its robustness.