中文摘要：

关键文字集影响判定布尔公式可满足性的判定难度。如果能找到公式的关键文字集或关键文字集的子集,就可使公式的可满足性判定变得容易。通过对警示传播算法的原理分析,发现高概率决定的部分变元对公式的求解难度有一定的影响。当某个子句与变元之间的警示信息具有一致性时,表明该子句的可满足性完全由该变元的取值决定,其它变元的取值都不能使得该子句可满足。进一步研究发现,当该算法收敛时,具有一致性的警示信息对应的变元集合是关键文字集的子集,这就佐证了警示传播算法可用于求解公式的关键文字集。基于该算法的特征,给出了一个寻找公式关键文字集的信息传播算法。

英文摘要：

The difficulty of solving Boolean formulae is mainly decided by the key literals.If the key literals or subset of formulas could be found,they would be tractable to solve the formula.The principle of the warning propagation was studied,and it was found that the decision part variables of high probability were important for solving the Boolean formulae.It was also found that if the warning message had consistency between the clause and variable,the variable could decide the clause satisfiability,while other variables did not contribute to satisfiability of the clause.Furthermore,it was proved that the part variables were the subset of the key literals when the warning propagation was convergent,which showed that the warning propagation could be used to find the key literals for the formulae.Finally,the massage passing algorithm to find the key literals was given by the warning propagation characterization.