Journal of Computer Applications ›› 2017, Vol. 37 ›› Issue (12): 3487-3492.DOI: 10.11772/j.issn.1001-9081.2017.12.3487
Previous Articles Next Articles
LIU Yanli1,2, XU Zhenxing2, XIONG Dan1
Received:
2017-06-07
Revised:
2017-08-03
Online:
2017-12-10
Published:
2017-12-18
Supported by:
通讯作者:
刘燕丽
作者简介:
刘燕丽(1980-),女,河南西平人,讲师,硕士,CCF会员,主要研究方向:NP问题的算法设计、算法优化;徐振兴(1990-),男,湖北鄂州人,博士研究生,主要研究方向:NP问题的近似求解、算法优化;熊丹(1979-),女,湖北天门人,讲师,硕士,主要研究方向:数理统计、系统辨识。
基金资助:
CLC Number:
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.
刘燕丽, 徐振兴, 熊丹. 基于动态奖惩的分支策略的SAT完备算法[J]. 计算机应用, 2017, 37(12): 3487-3492.
Add to citation manager EndNote|Ris|BibTeX
URL: http://www.joca.cn/EN/10.11772/j.issn.1001-9081.2017.12.3487
[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. |
[1] | Fan PING, Xiaochun TANG, Yanyu PAN, Zhanhuai LI. Scheduling strategy of irregular tasks on graphics processing unit cluster [J]. Journal of Computer Applications, 2021, 41(11): 3295-3301. |
[2] | Ying LEI, Wanbo ZHENG, Wei WEI, Yunni XIA, Xiaobo LI, Chengwu LIU, Hong XIE. Task offloading method based on probabilistic performance awareness and evolutionary game strategy in “cloud + edge” hybrid environment [J]. Journal of Computer Applications, 2021, 41(11): 3302-3308. |
[3] | Gangzhu QIAO, Rui WANG, Chaoli SUN. Improved high-dimensional many-objective evolutionary algorithm based on decomposition [J]. Journal of Computer Applications, 2021, 41(11): 3097-3103. |
[4] | Fumin ZOU, Sijie LUO, Zhihui CHEN, Lyuchao LIAO. Time-space distribution identification method of taxi shift based on trajectory data [J]. Journal of Computer Applications, 2021, 41(11): 3376-3384. |
[5] | . Hybrid adaptive large neighborhood search algorithm for solving time-dependent vehicle routing problem in cold chain logistics [J]. Journal of Computer Applications, 0, (): 0-0. |
[6] | . Alternately optimizing algorithm based on Brownian movement and gradient information [J]. Journal of Computer Applications, 0, (): 0-0. |
[7] | . Fault diagnosis method based on improved one-dimensional convolution and bidirectional long short-term memory neural network [J]. Journal of Computer Applications, 0, (): 0-0. |
[8] | . Yin-Yang-pair algorithm based on dynamic D-way splitting strategy and chaos perturbation [J]. Journal of Computer Applications, 0, (): 0-0. |
[9] | . Harris hawks optimization algorithm based on chemotaxis correction [J]. Journal of Computer Applications, 0, (): 0-0. |
[10] | . Influence maximization algorithm based on node coverage and structural holes [J]. Journal of Computer Applications, 0, (): 0-0. |
[11] | TANG Andi, HAN Tong, XU Dengwu, XIE lei. Chaotic elite Harris hawks optimization algorithm [J]. Journal of Computer Applications, 2021, 41(8): 2265-2272. |
[12] | LI Mengmeng, QIN Wei, LIU Yi, DIAO Xingchun. Hybrid ant colony optimization algorithm with brain storm optimization [J]. Journal of Computer Applications, 2021, 41(8): 2412-2417. |
[13] | ZHANG Wenqiang, XING Zheng, YANG Weidong. Hybrid particle swarm optimization with multi-region sampling strategy to solve multi-objective flexible job-shop scheduling problem [J]. Journal of Computer Applications, 2021, 41(8): 2249-2257. |
[14] | ZHANG Xiangfei, LU Yuming, ZHANG Pingsheng. Constrained multi-objective optimization algorithm based on coevolution [J]. Journal of Computer Applications, 2021, 41(7): 2012-2018. |
[15] | ZHANG Meng, LI Weihua. Influence maximization algorithm based on user interactive representation [J]. Journal of Computer Applications, 2021, 41(7): 1964-1969. |
Viewed | ||||||
Full text |
|
|||||
Abstract |
|
|||||