摘要
针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略。首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元。在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7。实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2%~29.3%,少数算例剪枝率的提高可达51%,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7%以上。所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间。
The limited number and high similarity of learning clauses lead to limited historical information and imbalanced search tree. In order to solve the problems, a dynamic branching strategy of award and punishment was proposed. Firstly, the variables of every unit propagation were punished. Different penalty functions were established according to whether the variable generated a conflict and the conflict interval. Then, in the learning phase, the positive variables for the conflict were found according to the learning clauses, and their activities were nonlinearly increased. Finally, the variable with the maximum activity was chosen as the new branching variable. On the basis of the glucose3.0 algorithm, an improved dynamic algorithm of award and punishment named Award and Punishment 7 （AP7） was completed. The experimental results show that, compared with the glucose3.0 algorithm, the rate of cutting branches of AP7 algorithm is improved by 14.2% - 29.3%, and that of a few examples is improved up to 51%. The running time of the improved AP7 algorithm is shortened more than 7% compared with the glucose3.0 algorithm. The branching strategy can efficiently reduce the size of search tree, make the search tree more balanced and reduce the comoutation time.
出处
《计算机应用》
CSCD
北大核心
2017年第12期3487-3492,共6页
journal of Computer Applications
基金
湖北省教育厅科学研究计划项目(B2016015)~~
关键词
NP完全问题
可满足性问题
冲突驱动子句学习
完备算法
分支策略
Non-deterministic Polynomial Complete problem （NPC）
SATisfiability problem （SAT）
conflict drivenclause learning
exact algorithm
branching strategy
