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

摘要：

利用极小不可满足公式的临界特性,可以将任意的一个3-CNF公式多项式时间归约转换为一个正则(3,4)-CNF公式,从而得到一个保留NP完全性的正则(3,4)-SAT问题.警示传播算法(Warning Propagation,WP)在归约转换后的正则(3,4)-SAT实例集上高概率收敛,但在任意一个实例上都无法判断公式的可满足性,因此算法求解失效.对于一个归约转换后的正则(3,4)-CNF公式,每一变元出现的正负次数之差具有趋于稳定的结构特征,基于该特征,提出基于变元正负出现次数规则的WP算法来求解归约转换后的正则(3,4)-SAT实例.实验结果表明,修正的WP算法对正则公式的可满足性判定有效,从而可以利用公式的正则性特征进一步研究WP算法的收敛性特征条件.

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

所属期刊栏目：45

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金项目61762019,61462001

在线出版日期：2018-12-17（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：312-317