求解SAT问题的拟人退火算法

该文利用一个简单的变换，将可满足性（SAT）问题转换为一个求相应目标函数最小值的优化问题，提出了一种用于跳出局部陷阱的拟人策略，基于模拟退火算法和拟人策略，为SAT问题的高效近注解得出了拟人退火算法（PA），该方法不仅具有模拟退火算法的全局收敛性质，而且具有一定的并行性，继承性。数值实验表明，对于本文随机产生的测试问题例，采用拟人策略的模拟退火算法的结果优于局部搜索算法，模拟退火算法以及近来国际上流行的WALKSAT算法，因此拟人退火算法是可行的和有效的。

Personification Annealing Algorithm for Solving SAT Problem

The satisfiability (SAT) problem is core topic of the fields of artificial intelligence and computer science. Therefore, algorithms to solve the SAT problem play an important role in the development of computing theory and systems. Traditional algorithms treat the SAT problem as a constrained decision problem. In this paper, we transform the SAT problem into a global optimization problem to the objective function by a simple transformation, thus many algorithms can be used to solve it. The SA algorithm is a general stochastic search algorithm for combinatorial optimization problems, however, this algorithm need often cost too much time for finding a solution, which prevents it from being applied to many practical problems. How to improve this algorithm for solving the SAT problem is what this paper concerns. In this paper, the personification strategies obtained by observing and learning from the social and nature phenomena are presented. These strategies are generally straightforward and intuitive, and are helpful for the search process jumping out of local minimum, thus allow simulated annealing process to converge fast. These strategies explained how to select variables to flip in each iterative step and how to raise the system temperature when the search process got stuck the local minimum. Combining the simulated annealing algorithm and proposed personification strategies, we present a personification annealing (PA) algorithm for solving the SAT problem. The PA algorithm inherits the global convergence property from simulated annealing algorithm and has the property of parallelism and inheritance. In order to compare the PA algorithm with local search algorithm,simulated annealing algorithm and WALKSAT algorithm, a C implementation of these algorithms was tested on random generated 3 SAT problem instances. The actual computational results show that the PA algorithm outperforms completely local search algorithm,simulated annealing algorithm and WALKSAT algorithm which is very popular recently, therefore the PA algorithm is feasible and efficient.