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

doi:10.11772/j.issn.1001-9081.2017.12.3487

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

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

刘燕丽^1,2, 徐振兴², 熊丹¹

1. 武汉科技大学理学院, 武汉 430081;
2. 华中科技大学计算机科学与技术学院, 武汉 430074

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

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

LIU Yanli^1,2, XU Zhenxing², XIONG Dan¹

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-18 Published:2017-12-10
Supported by:
This work is partially supported by the Science and Technology Project of Hubei Provincial Education Department (B2016015).

摘要/Abstract

摘要： 针对学习子句数量有限或相似度高导致历史信息有限、搜索树不平衡的问题，提出了基于动态奖惩的分支策略。首先，对每次单子句传播的变元进行惩罚，依据变元是否产生冲突和产生冲突的间隔，确立不同的惩罚函数；其次，在学习阶段，利用学习子句确定对构造冲突有益的变元，非线性增加它们的活跃度；最后，选择活跃度最大的变元作为新分支变元。在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

中图分类号:

TP301.6

刘燕丽, 徐振兴, 熊丹. 基于动态奖惩的分支策略的SAT完备算法[J]. 计算机应用, 2017, 37(12): 3487-3492.

LIU Yanli, XU Zhenxing, XIONG Dan. Exact SAT algorithm based on dynamic branching strategy of award and punishment[J]. Journal of Computer Applications, 2017, 37(12): 3487-3492.

参考文献

[1] DAVIS M, LOGEMANN G, LOVELAND D. A machine program for theorem proving[J]. Communications of the ACM, 1962, 5(7):394-397.
[2] MOSKEWICZ M W, MADIGAN C F, ZHAO Y, et al. Chaff:engineering an efficient sat solver[C]//Proceedings of the 38th Annual Design Automation Conference. New York:ACM, 2001:530-535.
[3] ANSÓTEGUI C, BONET M L, LEVY J. SAT-based MaxSAT algorithms[J]. Artificial Intelligence, 2013, 196:77-105.
[4] KOSHIMURA M, ZHANG T, FUJITA H, et al. QMaxSAT:a partial Max-SAT solver system description[J]. Journal on Satisfiability, Boolean Modeling and Computation, 2012, 8(1/2):95-100.
[5] ZHANG L T, MADIGAN C F, MOSKEWICZ M H, et al. Efficient conflict driven learning in a boolean satisfiability solver[C]//ICCAD 2001:Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design. Piscataway, NJ:IEEE, 2001:279-285.
[6] LIU Y L, LI C M, HE K, et al. Breaking cycle structure to improve lower bound for Max-SAT[C]//FAW 2016:Proceeding of the 11th International Workshop on Frontiers in Algorithmics, LNCS 9711. Berlin:Springer, 2016:111-124.
[7] AUDEMARD G, SIMON L. Predicting learnt clauses quality in modern SAT solvers[C]//IJCAI 2009:Proceeding of the 2009 International Joint Conference on Artificial Intelligence. San Francisco, CA:Morgan Kaufmann, 2009:399-404.
[8] AUDEMARD G, LAGNIEZ J M, SIMON L. Improving glucose for incremental SAT solving with assumption:application to MUS extraction[C]//SAT 2013:Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing. Berlin:Springer, 2013:309-317.
[9] DE KLERK E. Aspects of Semidefinite Programming[M]. Berlin:Springer, 2002:211-228.
[10] 刘燕丽,李初民,何琨.基于优化冲突集提高下界的MaxSAT完备算法[J].计算机学报,2013,36(10):2087-2095.(LIU Y L, LI C M, HE K. Improved lower bounds in MAXSAT complete algorithm based optimizing inconsistent set[J]. Chinese Journal of Computers, 2013, 36(10):2087-2095.)
[11] 刘燕丽,黄飞,张婷.基于环型扩展推理规则的MaxSAT完备算法[J].南京大学学报(自然科学版),2015,51(4):762-771.(LIU Y L, HUANG F, ZHANG T. MaxSAT complete algorithm based cycle extended inference rules[J]. Journal of Nanjing University (Natural Sciences), 2015, 51(4):762-771.)
[12] AUDEMARD G, SIMON L. Lazy clause exchange policy for parallel SAT solvers[C]//SAT 2014:Proceedings of the 201417th International Conference on Theory and Applications of Satisfiability Testing, LNCS 8561. Berlin:Springer, 2014:197-205.

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

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

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 9

编辑推荐

Metrics

[1]	庞立超, 王晓峰, 谢志新, 杨易, 赵星宇, 杨澜. 随机正则3-可满足性问题的解簇结构分析[J]. 《计算机应用》唯一官方网站, 2024, 44(7): 2137-2143.
[2]	赵星宇, 王晓峰, 杨易, 庞立超, 杨澜. 求解恰当可满足性问题的随机局部搜索算法[J]. 《计算机应用》唯一官方网站, 2024, 44(3): 842-848.
[3]	武小年, 匡晶, 张润莲, 李灵琛. 基于SAT的GRANULE算法不可能差分分析[J]. 《计算机应用》唯一官方网站, 2024, 44(3): 797-804.
[4]	彭庆媛, 王晓峰, 王军霞, 华盈盈, 唐傲, 何飞. 可满足性问题相变研究综述[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3503-3512.
[5]	许秀兰李克清黄瑜岳. 无线传感器网络中基于动态规划的节点高效部署算法[J]. 计算机应用, 2013, 33(11): 3024-3027.
[6]	冯登科阮奇杜利敏. 二进制布谷鸟搜索算法[J]. 计算机应用, 2013, 33(06): 1566-1570.
[7]	孙伟李艳灵鲁骏. 基于Partial MAX-SAT求解法的RBAC授权查询方法[J]. 计算机应用, 2013, 33(05): 1367-1390.
[8]	李玮王雷. 中国邮递员问题的DNA计算[J]. 计算机应用, 2009, 29(07): 1880-1883.
[9]	潘达儒，杜明辉. 基于神经网络和遗传算法的组播路由算法[J]. 计算机应用, 2005, 25(06): 1261-1263.