1. School of Information Science and Technology, Southwest Jiaotong University, Chengdu 610031, China; 2. National-Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 610031, China; 3. School of Mathematics, Southwest Jiaotong University, Chengdu 610031, China
Abstract：To improve solving efficiency for SAT (boolean satisfiability) problems,a combination of genetic algorithm (GA) with local search algorithm (LSA) on the OpenMP (open multi-processing) framework was proposed. This combination improved the selection algorithm in the hybrid genetic algorithm (HGA) and reduced the time complexity of the original selection operation to O(N). The compiler guide statement #pragma omp parallel in OpenMP was applied to coarse-grained parallelization driven HGA,and the #pragma omp single statement block was used to implement the synchronization migration operation of the individuals in different sub-groups. Compared with the similar algorithm,HCGA (hybrid cloud genetic algorithm),both the improved algorithm (HGA) and the coarse-grained parallel hybrid genetic algorithm (CGPHGA) significantly improved solution success rate and problem solving efficiency. Solution success rate for some problems was increased by 5 times.
黄拙,张健. 由一阶逻辑公式得到命题逻辑可满足性问题实例[J]. 软件学报,2005,16(3):329-325 HUANG Zhuo, ZHANG Jian. Generating SAT instances from first-order formulas[J]. Journal of Software, 2005, 16(3):329-325
[2]
LI Bingfen,ZHANG Y A. A hybrid genetic algorithm to solve 3-SAT problem.[C]//201612th International Conference on Natural Computation,Fuzzy Systems and Knowledge Discovery. Changsha:IEEE Press,2016:476-480
[3]
潘晓英,焦李成,刘芳. 求解SAT问题的多智能体社会进化算法[J]. 计算机学报,2014,37(9):2011-2020 PAN Xiaoying, JIAO Licheng, LIU Fang. A multi-agent social evolutionary algorithm for SAT problem[J]. Chinese Journal of Computers, 2014, 37(9):2011-2020
[4]
LUO Chuan,CAI Shaowei,WU Wei,et al. Double configuration checking in stochastic local search for satisfiability[C]//Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. Québec City:AAAI,2014:2703-2709
[5]
郭莹,张长胜,张斌. 求解SAT问题的算法的研究进展[J]. 计算机科学,2016,43(3):8-17 GUO Ying, ZHANG Changsheng, ZHANG Bin. Research advance of SAT solving algorithm[J]. Computer Science, 2016, 43(3):8-17
[6]
HOLLAND J H. Adaptation in natural and artificial systems[M]. Cambridge:MIT press,1992:159-171
[7]
DE JONG K A. The analysis of the behavior of a class of genetic adaptive systems[D]. Ann Arbor:University of Michigan,1975
[8]
GOLDBERG D E. Genetic algorithms in search optimization and machine learning[J]. Machine Learning, 1988, 3(2):95-99
[9]
张琛,詹志辉. 遗传算法选择策略比较[J]. 计算机工程与设计,2009,30(23):5471-5474,5478 ZHANG Chen, ZHAN Zhihui. Comparisons of selection strategy in genetic algorithm[J]. Computer Engineering and Design, 2009, 30(23):5471-5474,5478
[10]
高家全,何桂霞. 并行遗传算法研究综述[J]. 浙江工业大学学报,2007(1):56-59,72 GAO Jiaquan, HE Guixia. A review of parallel genetic algorithms[J]. Journal of Zhejiang University of Technology, 2007(1):56-59,72
[11]
ROBERGE V, TARBOUCHI M, LABONTE G. Comparison of parallel genetic algorithm and particle swarm optimization for real-time UAV path planning[J]. IEEE Trans. Industrial Informatics, 2013, 9(1):132-141
[12]
CALEGARI P, GUIDEC F, KUONEN P, et al. Parallel island-based genetic algorithm for radio network design[J]. J. Parallel Distrib. Comput, 1997, 47(1):86-90
[13]
YANG Hongtai, YANG Paichuan, HUANG Chinglien. A parallel genetic algorithm approach to solving the unit commitment problem:Implementation on the transputer networks[J]. IEEE Transactions on Power Systems, 1997, 12(2):661-668
[14]
TIMOTHY G. MATTSON B S,BERNA M. Patterns for parallel programming[M].[S.l.]:Pearson Education,2004:76-78
[15]
ASGHAR S,AUBANEL E,BREMNER D. A dynamic moldable job scheduling based parallel SAT solver[C]//201342nd International Conference on Parallel Processing (ICPP).[S.l.]:IEEE,2013:110-119
[16]
HAMADI Y, JABBOUR S, SAIS L. ManySAT:a parallel SAT solver[J]. Journal on Satisfiability,Boolean Modeling and Computation, 2008, 1(6):245-262
[17]
WU Guanfeng,XU Yang,CHANG Wenjing,et al. Parallel genetic algorithm for SAT problems based on the coarse-grained model[C]//Uncertainty Modelling in Knowledge Engineering and Decision Making:Proceedings of the 12th International FLINS Conference. Roubaix:Springer,2016:489-495
[18]
MASTSUMURA T, NAKAMURA M, OKENCH J, et al. A parallel and distributed genetic algorithm on loosely-coupled multiprocessor systems[J]. IEICE Transactions on Fundamentals of Electronics,Communications and Computer Sciences, 1998, 81(4):540-546
[19]
BECKERSM L M, DERKS EPPA, MELSSEN W J, et al. Using genetic algorithms for conformational analysis of biomacromolecules[J]. Computers & Chemistry, 1996, 20(4):449-457
[20]
岳嵚. 粗粒度并行遗传算法的计算性能及其应用研究[D]. 武汉:华中科技大学,2008
[21]
MENOUER T,BAARIR S. Parallel satisfiability solver based on hybrid partitioning method[C]//201725th Euromicro International Conference on Parallel,Distributed and Network-based Processing.[S.l.]:IEEE,2017:54-60
[22]
LAYEB A, SAIDOUNI D E. A hybrid quantum genetic algorithm and local search based DPLL for max 3-SAT problems[J]. Applied Mathematics & Information Sciences, 2014, 8(1):77-87
[23]
ROLI,A. Criticality and parallelism in structured SAT instances[C]//International Conference on Principles and Practice of Constraint Programming. Berlin:Springer,2002,714-719
[24]
ZHANG Wenhui,HUANG Zhuo,ZHANG Jian. Parallel execution of stochastic search procedures on reduced SAT instances[C]//Pacific Rim International Conference on Artificial Intelligence. Berlin:Springer,2002:108-117
