Computer Science ›› 2019, Vol. 46 ›› Issue (11A): 19-22.

• Intelligent Computing • Previous Articles     Next Articles

Branching Strategy Based on Weighted Decision Variable Level

WANG Meng, HE Xing-xing   

  1. (School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China)
  • Online:2019-11-10 Published:2019-11-20

Abstract: In order to improve the solution efficiency of CDCL solver,for the choice of decision variable problem of the satisfiability (SAT) problem algorithm,a kind of branching strategy based on weighted decision variable level was proposed.The main idea of the new strategy is based on the boolean constraint propagation (BCP) back track and restart mechanism in the process.Firstly,the number of variables used as decision variables and the decision-making level are considered.Secondly,due to the selected number of variables and the difference in the decision-making level,the weight of variables is considered to be different.Finally,in combination with the conflict analysis process,the variables are rewarded and scored.The scores of different variables in the new strategy are compared with those in the VSIDS and EVIDS strategies.A large number of examples in SATLIB (SAT Little Information Bank) are used for experimental testing,and the results show that the new strategy can reduce the number of conflicts and the solution time (CPU),and improve the solving efficiency of the solver.

Key words: Conflicts, Decision level, Decision variables, Restart, Weighed

CLC Number: 

  • TP301
[1]王国俊.数理逻辑引论与归结原理[M].北京:科学出版社,2007:23-24.
[2]COOK S A.The complexity of theorem proving procedures[C]∥Proceedings of the ACM SymPosium on Theory of Computin.Shaker Heights,1971:151-158.
[3]SILVA J P M,SAKALLAH K A.GRASP:a new search algorithm for satisfiability[C]∥Proceedings of the IEEE/ACM International Conference on Computer-Aided Design.Los Alamitos,2002:220-227.
[4]JEROSLOW R G,WANG J.Solving propositional satisfiability problems[J].Annals of Mathematics and Artificial Intelligence,1990,1(1/2/3/4):167-187.
[5]FREEMAN J W.Improvements to propositional satisfiability search algorithms[D].Philadelphia:University of Pennsylvania,1995.
[6]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A new search algorithm for satisfiability[C]∥International Conference on Computer Aided Design.1996:220-227.
[7]MOSKEWICZ M W,MADIGAN C F,ZHAO Y,et al.Chaff:engineering an efficient SAT solver[C]∥Proceedings of the 38th Design Automation Conference.New York:ACM,2001:530-535.
[8]LIANG J H,GANESH V,POUPART P,et al.Learning rate based branching heuristic for SAT solvers[C]∥Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing(SAT 2016).2016:123-140.
[9]AUDEMARD G,SIMON L.Predicting learnt clauses quality in modern SAT solvers[C]∥Proceedings of the 21st International Joint Conference on Artificial Intelligence(IJCAI 2009).2009:399-404.
[10]MARQUES-SILVA J P,SAKALLAH K A.GRASP:A search algorithm for propositional satisfiability[J].IEEETransactions on Computers,1999,48(5):506-521.
[11]DAVIS M,LOGEMANN G,LOVELAND D.A machine program for theorem proving[J].Communications of the ACM,1962,59(5):394-397.
[12]BURO M,KLEINE-BÜNING H.Report on a SAT competition[J].Bulletin of the European Association for Theoretical Computer Science,1993,5(2):49.
[13]MALIK S,ZHAO Y,MADIGAN C F.Chaff:an efficient SAT solver[C]∥Proceedings of the Design Automation Conference.LasVegas,2001:530-535.
[14]SELMAN B,KAUTZ H,MCALLESTER D.Ten challenges in propositional reasoning and search[C]∥Proceedings of the 15 the International Conference on Artificial Intelligence.Aichi,1997:50-54.
[15]JEROSLOW R G,WANG J.Solving propositional satisfiabilityproblems[J].Annals of Mathematics & Artificial Intelligence,1990,1(1/2/3/4):167-187.
[16]MARQUES-SILVA JP,SAKALLAH K A.Grasp:a new search algorithm for satisfiability[C]∥Proceedings of the 1996 IEEE/ACM International Conference on Computeraided Design.Los Alamitos:IEEE Computer Society Press,1996:220-227.
[17]GOMES C P,SELMAN B,CRATO N.Heavy-tailed distributions in combinatorial search[C]∥Proceedings of the International Conference on Principles and Practice of Constraint Programming.Linz,1997:121-135.
[18]EÉN N,SÖRENSSON N.An Extensible SAT-solver[M]∥Theory and Applications of Satisfiability Testing.Santa Margherita Ligure,2003:502-518.
[19]BIERE A,FRÖHLICH A.Evaluating CDCL Variable ScoringSchemes[C]∥International Conference on Theory and Applications of Satisfiability Testing.Cham:Springer,2015:405-422.
[20]ZHANG L,MADIGAN C,MOSKEWICZ M,et al.EfficientConflict Driven Lening in a Boolean Satisfiability Slover[C]∥International Conferenceon Computer Aided Sesign (ICCAD).SanJose CA,2001.
[1] CHEN Qing-shan, XU Yang, WU Guan-feng and HE Xing-xing. Path Identification Based Delaying Restart Algorithm for CDCL SAT Solver [J]. Computer Science, 2017, 44(11): 279-283.
[2] YANG Jin-cai,XIE Fang and HU Jin-zhu. Research on Rule Engine for Automatic Identification of Relational Words in Chinese Complex Sentences [J]. Computer Science, 2014, 41(Z11): 25-28.
[3] . Branch Predictor with TBHBP Based on Simultaneous Multithreaded Processors [J]. Computer Science, 2012, 39(9): 307-311.
[4] LI Lin, LU Xian-Liang. Test Pac(}ets Choice Algorithm Aiming at Filter Conflicts [J]. Computer Science, 2011, 38(9): 71-75.
[5] GUO Yu-tang. Automatic Image Annotation Method and Fast Solution Based on the Mutual K Nearest Neighbor Graph [J]. Computer Science, 2011, 38(2): 277-280.
[6] WU Hai, CHEN Wei, LU Yan-sheng (Computer College, Huazhong University of Science and Technology, Wuhan 430074, China). [J]. Computer Science, 2009, 36(2): 155-157.
[7] . [J]. Computer Science, 2008, 35(8): 101-103.
[8] GUAN Zhong (Guangzhou City Polytechnic, Guangzhou 510230). [J]. Computer Science, 2007, 34(6): 58-60.
[9] WANG Zhan ZHAO Yan-Li LIU Feng-Yu ZHANG Hong (Department of Computer, Nanjing University of Science and Technology, Nanjing 210094). [J]. Computer Science, 2007, 34(12): 265-267.
[10] WANG Zhan ,YOU Jing, ZHAO Yan-Li ,LIU Feng-Yu ,ZHANG Hong (Department of Computer, Nanjing University of Science and Technology,Nanjing 210094). [J]. Computer Science, 2006, 33(9): 274-277.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!