基于子句权重学习的求解SAT问题的遗传算法

Genetic Algorithm for Solving SAT Problems Based on Learning Clause Weights

该文提出了一种求解SAT问题的改进遗传算法(SATWAGA).SATWAGA算法有多个改进性特点:将SAT问题的结构信息量化为子句权重,增加了学习算子和判定早熟参数,学习算子能根据求解过程中的动态信息对子句权重进行调整,以便防止遗传进程的早熟,同时,算法还采用了最优染色体保存策略,防止进化过程的发散.该文最后描述了实现包括SATWAGA等多个算法的实验系统,对选择最佳早熟判定参数值给出了一些有效的建议.实验结果表明:与一般遗传算法相比,SATWAGA算法在求解速度、成功率和求解问题的规模等方面都有明显的改善.

A novel genetic algorithm, SAT-WAGA, is proposed for solving SAT problems based on learning clause weights in this paper. Several new characteristics of the algorithm are innovative. The new algorithm makes use of the heuristic information from the structure of SAT problems by clause weights. A new operator of learning clause weights is designed to prevent precocity in the process of solving problems. This operator adapts the weights of clauses according to a criteria condition. A criteria parameter for detecting precocity is defined. The strategy of keeping the best chromosomes guarantees the property of convergence in the evolution iteration. To demonstrate the feasibility of the new algorithm, an experiment system of several famous algorithms is implemented. The experiment works focus on comparing the total span of all plateaus in evolution iteration, the success rates and the total time of the new algorithm to a classical genetic algorithm by solving several groups of various scales of random generated SAT problem instances. The appropriate values of the precocity criteria parameter of the new algorithm are also tested and presented. The experimental results show that the SAT-WAGA performs remarkably better than a classical genetic algorithm in the aspects of speed, the success rate and the solvable problem scales.