基于关键文字的求解SAT问题的启发式算法

A Heuristic Algorithm for Solving the Satisfiability Problem Based on the Key Literal

逻辑公式的可满足问题的求解方法是近几年研究的重点,通过对逻辑公式的关键文字和骨干变元集的研究与分析,使用启发式算法寻找公式的关键文字,在公式化简中引入关键文字规则,给出了一种新的求解SAT问题的启发式算法。

The solution method of the satisfiability problem of the logic formula is the focus of the study in recently years.Through the study and analysis of the key word and backbone of the logic formula,using the heuristic algorithm to search the key literal of the formula,introducing the rule of the key literal into the simplification of the formula,and giving out a new heuristic algorithm for the satisfiability problem.