Abstract: Currently local search algorithms are very effective for solving some SAT problems, and Sattime is a typical local search algorithm which won a silver medal in the 2011 international SAT competition. But, after recording the variable flipping event data stream into a database in the solving process of Sattime algorithm, data analysis and pattern mining uncover that Sattime sometimes selects the same variable to flip in two successive flipping steps. This search behavior may cause loop back and is known as the loopback phenomenon, which reduces the local search efficiency. To solve the problem, this paper proposes two probability control strategies：the enhanced strategy for choosing clause and the enhanced strategy for choosing variable. Applying these two strategies into Sattime algorithm, the paper develops a new local search algorithm called Sattime-P. Experimental results show that the improved algorithm Sattime-P is more efficient in most cases. Moreover, this method can also be applied to other SAT local search algorithms to improve their efficiency.

Key words: SAT problem, local search, probability controlled, clause, Bool variable

摘要： 局部搜索算法是目前求解SAT问题比较有效的方法，而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中，记录变元翻转事件流数据库，通过数据分析与模式挖掘，发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象，即所谓的回环现象，从而降低了求解效率。为解决此问题，提出两种概率控制策略：加强子句选择策略和加强变元选择策略，并将这两种策略应用到Sattime算法中，形成新的局部搜索算法Sattime-P。实验结果表明，与Sattime算法相比，改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。

关键词: SAT问题, 局部搜索, 概率控制, 子句, 布尔变元