一种基于加权决策变量决策层的分支策略

摘要/Abstract

摘要： 为了提高CDCL求解器的求解效率,针对可满足性(SAT)问题算法中决策变量的选择问题,提出了一种基于加权决策变量决策层的分支策略。这个新策略的主要思想是:基于布尔约束传播(BCP)过程中的回溯以及重启机制,首先考虑变量作为决策变量的次数以及所在决策层;其次,由于被选择的次数以及所在决策层不同,即占权重不同,对此进行加权;最后,结合冲突分析过程,对不同的变量给予不同的奖励得分。将不同变量在新策略与VSIDS和EVIDS策略中的得分进行对比,采用SATLIB(SAT Little Information Bank)中的大量例子进行实验测试,结果表明,新策略能够减少冲突次数以及求解时间(cpu),提高了求解器的求解效率。

关键词: 冲突, 加权, 决策变量, 决策层, 重启

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

中图分类号:

TP301

王萌, 何星星. 一种基于加权决策变量决策层的分支策略[J]. 计算机科学, 2019, 46(11A): 19-22. https://doi.org/

WANG Meng, HE Xing-xing. Branching Strategy Based on Weighted Decision Variable Level[J]. Computer Science, 2019, 46(11A): 19-22. https://doi.org/

参考文献

[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.

相关文章 15

[1]	杨文坤, 原晓佩, 陈小锋, 郭睿. 三维激光雷达点云空间多特征分割 Spatial Multi-feature Segmentation of 3D Lidar Point Cloud 计算机科学, 2022, 49(8): 143-149. https://doi.org/10.11896/jsjkx.210300275
[2]	石先让, 宋廷伦, 唐得志, 戴振泳. 一种新颖的单目视觉深度学习算法:H_SFPN Novel Deep Learning Algorithm for Monocular Vision:H_SFPN 计算机科学, 2021, 48(4): 130-137. https://doi.org/10.11896/jsjkx.200400090
[3]	储杰, 张正军, 汤鑫瑶, 黄振生. 基于加权样本和共识率的标记传播算法 Label Propagation Algorithm Based on Weighted Samples and Consensus-rate 计算机科学, 2021, 48(3): 214-219. https://doi.org/10.11896/jsjkx.191200103
[4]	张子良, 庄毅, 叶彤. 基于元模型的协同建模模型组装与更新方法 Cooperative Modeling Model Combination and Update Method Based on Meta-model 计算机科学, 2021, 48(12): 67-74. https://doi.org/10.11896/jsjkx.201100024
[5]	张天瑞, 魏铭琦, 高秀秀. 基于IPSO-WRF的选择性激光烧结件气泡溶解时间预测模型 Prediction Model of Bubble Dissolution Time in Selective Laser Sintering Based on IPSO-WRF 计算机科学, 2021, 48(11A): 638-643. https://doi.org/10.11896/jsjkx.210300080
[6]	刘丹, 赵森, 颜志良, 赵静, 王会青. 基于堆叠自动编码器的miRNA-疾病关联预测方法 miRNA-disease Association Prediction Model Based on Stacked Autoencoder 计算机科学, 2021, 48(10): 114-120. https://doi.org/10.11896/jsjkx.200900169
[7]	朱珍, 黄锐, 臧铁钢, 卢世军. 基于加权近红外图像融合的单幅图像除雾方法 Single Image Defogging Method Based on Weighted Near-InFrared Image Fusion 计算机科学, 2020, 47(8): 241-244. https://doi.org/10.11896/jsjkx.200300068
[8]	姜辰凯, 李智, 盘书宝, 王勇军. 基于改进Dijkstra算法的AGVs无碰撞路径规划 Collision-free Path Planning of AGVs Based on Improved Dijkstra Algorithm 计算机科学, 2020, 47(8): 272-277. https://doi.org/10.11896/jsjkx.190700138
[9]	沈雪, 陈树伟, 艾森阳. 基于奖励机制的SAT求解器分支策略 Reward Mechanism Based Branching Strategy for SAT Solver 计算机科学, 2020, 47(7): 42-46. https://doi.org/10.11896/jsjkx.190700191
[10]	宋传鸣, 洪旭, 王相海. 空-频域联合投票的交通视频阴影去除方法 Shadow Removal of Traffic Surveillance Video by Joint Voting in Spatial-Frequency Domain 计算机科学, 2020, 47(5): 129-136. https://doi.org/10.11896/jsjkx.190400040
[11]	朱莹,夏亦犁,裴文江. 基于改进的BEMD的红外与可见光图像融合方法 Fusion of Infrared and Color Visible Images Based on Improved BEMD 计算机科学, 2020, 47(3): 124-129. https://doi.org/10.11896/jsjkx.190100038
[12]	吴甜甜,王洁. 基于可能回答集程序的多Agent信念协调 Belief Coordination for Multi-agent System Based on Possibilistic Answer Set Programming 计算机科学, 2020, 47(2): 201-205. https://doi.org/10.11896/jsjkx.190100101
[13]	古雪梅,刘嘉勇,程芃森,何祥. 基于增强BiLSTM-CRF模型的推文恶意软件名称识别 Malware Name Recognition in Tweets Based on Enhanced BiLSTM-CRF Model 计算机科学, 2020, 47(2): 245-250. https://doi.org/10.11896/jsjkx.190500063
[14]	刘志, 曹诗鹏, 沈阳, 杨曦. 基于改进深度强化学习方法的单交叉口信号控制 Signal Control of Single Intersection Based on Improved Deep Reinforcement Learning Method 计算机科学, 2020, 47(12): 226-232. https://doi.org/10.11896/jsjkx.200300021
[15]	张文华, 刘晓鸽, 王沛沛, 刘静静, 程敬亮. 肝脏多b值扩散加权图像的三维配准 3D Registration for Multi-b-value Diffusion Weighted Images of Liver 计算机科学, 2020, 47(11A): 241-243. https://doi.org/10.11896/jsjkx.200400060

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed