用于求解正则(3,4)-SAT实例集的修正警示传播算法  

Modified Warning Propagation Algorithm for Solving Regular(3,4)-SAT Instance Sets

作　　者：佘光伟 许道云[1] SHE Guang-wei;XU Dao-yun(College of Computer Science and Technology,Guizhou University,Guiyang 550025,China)

机构地区：[1]贵州大学计算机科学与技术学院,贵阳550025

出　　处：《计算机科学》2018年第11期312-317,共6页Computer Science

基　　金：国家自然科学基金项目(61762019;61462001)资助

摘　　要：利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题。警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高概率收敛,但在任意一个实例上都无法判断公式的可满足性,因此算法求解失效。对于一个归约转换后的正则(3,4)-CNF公式,每一变元出现的正负次数之差具有趋于稳定的结构特征,基于该特征,提出基于变元正负出现次数规则的WP算法来求解归约转换后的正则(3,4)-SAT实例。实验结果表明,修正的WP算法对正则公式的可满足性判定有效,从而可以利用公式的正则性特征进一步研究WP算法的收敛性特征条件。Based on the critical characterization of the minimal unsatisfiable formula,a 3-CNF formula can be reduced to a regular(3,4)-CNF formula within polynomial time.Thus the regular(3,4)-SAT problem is NP-complete.The war-ning propagation algorithm(WP)converges in high probability on the regular(3,4)-SAT instance sets by reducing,but it can’t determine the satisfiability of the formula on any instance,so the algorithm fails to solve the problem.For a reduced regular(3,4)-CNF formula,the difference between the positive and negative occurences of each variable has been found to be stable.With this feature,a WP algorithm based on the rule of positive and negative occurences was proposed to solve the reduced regular(3,4)-SAT instances.The experimental results show that the modified WP algorithm is effective for regular formulas.Therefore,the regularity of the formula can be used to study the convergence of the WP algorithm.

关 键 词：极小不可满足公式 正则(3 4)-SAT问题 警示传播算法 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]