DPLL算法中的变量决策启发式策略 Heuristic Strategies for Deciding Variables in DPLL Algorithm

针对命题公式φ(CNF形式)的可满足性问题的求解效率问题，基于对DPLL完全算法的学习和在不同形式下对子句文字排序处理的研究，提出了一种新的求解SAT问题的算法。新算法根据子句长度对命题公式φ进行分组，并根据变量出现次数进行初始排序，然后考虑变量中正负文字出现的次数，并对次数高的进行赋值。算法实例表明：新算法能减少求解过程中规则使用次数，减少求解步骤，尽早剪除不满足解空间，从而有效提高求解效率。 Aiming at the problem of the resolution efficiency of propositional satisfiability problem for propositional formula φ (CNF Form), based on the study of the DPLL complete algorithm and the research of the word order processing under different forms, a new algorithm for solving SAT problem is proposed. The algorithm groups propositional formula φ according to the length of clause, and sorts the words according to the number of polarity occurrence frequency in the initial sort. Then it considers the number of occurrences of the plus or minus words in variables and gets the value of high numbers. Algorithm instance shows that the new algorithm can reduce the number of rules in the process of using, reduce the solving steps, cut off the unsatisfy space of solution as soon as possible, so as to improve the solution efficiency.