计算机应用 ›› 2017, Vol. 37 ›› Issue (12): 3487-3492.DOI: 10.11772/j.issn.1001-9081.2017.12.3487

• 人工智能 • 上一篇    下一篇

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

刘燕丽1,2, 徐振兴2, 熊丹1   

  1. 1. 武汉科技大学 理学院, 武汉 430081;
    2. 华中科技大学 计算机科学与技术学院, 武汉 430074
  • 收稿日期:2017-06-07 修回日期:2017-08-03 出版日期:2017-12-10 发布日期:2017-12-18
  • 通讯作者: 刘燕丽
  • 作者简介:刘燕丽(1980-),女,河南西平人,讲师,硕士,CCF会员,主要研究方向:NP问题的算法设计、算法优化;徐振兴(1990-),男,湖北鄂州人,博士研究生,主要研究方向:NP问题的近似求解、算法优化;熊丹(1979-),女,湖北天门人,讲师,硕士,主要研究方向:数理统计、系统辨识。
  • 基金资助:
    湖北省教育厅科学研究计划项目(B2016015)。

Exact SAT algorithm based on dynamic branching strategy of award and punishment

LIU Yanli1,2, XU Zhenxing2, XIONG Dan1   

  1. 1. College of Science, Wuhan University of Science and Technology, Wuhan Hubei 430081, China;
    2. School of Computer Science and Technology, Huazhong University of Science and Technology, Wuhan Hebei 430074, China
  • Received:2017-06-07 Revised:2017-08-03 Online:2017-12-10 Published:2017-12-18
  • Supported by:
    This work is partially supported by the Science and Technology Project of Hubei Provincial Education Department (B2016015).

摘要: 针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题,提出了基于动态奖惩的分支策略。首先,对每次单子句传播的变元进行惩罚,依据变元是否产生冲突和产生冲突的间隔,确立不同的惩罚函数;其次,在学习阶段,利用学习子句确定对构造冲突有益的变元,非线性增加它们的活跃度;最后,选择活跃度最大的变元作为新分支变元。在glucose3.0算法基础上,完成了改进的动态奖惩算法——AP7。实验结果表明,相比glucose3.0算法,AP7算法的剪枝率提高了14.2%~29.3%,少数算例剪枝率的提高可达51%,且改进后的AP7算法相比glucose3.0算法,运行时间缩短了7%以上。所提分支策略可以有效降低搜索树规模,使搜索树更加平衡,减少计算时间。

关键词: NP完全问题, 可满足性问题, 冲突驱动子句学习, 完备算法, 分支策略

Abstract: 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 computation time.

Key words: Non-deterministic Polynomial Complete problem (NPC), SATisfiability problem (SAT), conflict driven clause learning, exact algorithm, branching strategy

中图分类号: