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

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