基于动态奖惩的分支策略的SAT完备算法

发布时间：2018-06-27 02:10

本文选题：NP完全问题 + 可满足性问题　；参考：《计算机应用》2017年12期

【摘要】：针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略。首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元。在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7。实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2%~29.3%,少数算例剪枝率的提高可达51%,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7%以上。所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间。
[Abstract]:Aiming at the problem that the limited number of learning clauses or the high similarity result in the limited historical information and the imbalance of search tree, a branch strategy based on dynamic rewards and punishments is proposed. First of all, the variables propagated by each single child sentence are punished, and different penalty functions are established according to whether the variables produce conflicts and the interval between them. Secondly, in the learning stage, learning clauses are used to determine the variables that are beneficial to the construction of conflicts. Finally, the most active variables are selected as new branch variables. On the basis of glucose3.0 algorithm, the improved dynamic reward and punishment algorithm AP7. The experimental results show that compared with glucose3.0 algorithm, the pruning rate of AP7 algorithm is increased by 14.2and 29.3s, the pruning rate of a few examples can be increased by 51%, and the running time of the improved AP7 algorithm is reduced by more than 7% compared with that of glucose3.0 algorithm. The proposed branching strategy can effectively reduce the size of the search tree, make the search tree more balanced and reduce the computing time.
【作者单位】：武汉科技大学理学院;华中科技大学计算机科学与技术学院;
【基金】：湖北省教育厅科学研究计划项目(B2016015)~~
【分类号】：TP301.6

【相似文献】