基于加权平均值的一种分支启发式方法

摘要/Abstract

摘要： 在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出一种基于加权平均值的分支启发式方法。该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较。由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、 SUM(Sum in experiment)策略和 ACIDS(Average Conflict-index Decision Score)策略。对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足。

关键词: 冲突次数, 分支启发式, 加权平均, 决策层, 序列

Abstract: The effective branching strategy was proposed in the satisfiability (SAT) problem algorithm,which can improve the efficiency of the solver.In consideration of the conflict,according to whether the variables join in conflict and conflict times,a branching heuristic method based on added weight average value was proposed.Firstly,a sequence is used to record whether the variables are involved in the conflict.Secondly,a weighted average function is given,the function value is calculated through variable sequences and decision levels.Finally,variable with the largest value is assigned,example analysis and comparisonare conducted.The new method is an improved method according to the control encoding method,so in the example analysis,the comparison and analysis ways were used,and SUM (Sum in experiment) strategy and ACIDS(Average Conflict-index Decision Score) strategy were compared with the new method at the same time.Through analysis of examples in SATLIB (SAT little information bank),the results show that more clauses are satisfied or the latest conflict clause can get the priority by the new method.

Key words: Branching heuristic, Decision layer, Sequence, Times of conflict, Weighted average

中图分类号:

TP181

胡忠雪, 徐扬, 胡容. 基于加权平均值的一种分支启发式方法[J]. 计算机科学, 2018, 45(11A): 117-120. https://doi.org/

HU Zhong-xue, XU Yang, HU Rong. Branching Heuristic Method Based on Added Weight Average Value[J]. Computer Science, 2018, 45(11A): 117-120. https://doi.org/

参考文献

[1]田奕,刘涛.求解可满足性问题的一种高效遗传算法[J].模式识别与人工智能,1996,9(3):209-212.
[2]WU G F,XU Y,CHANG W,et al.Parallel Genetic Algorithm for SAT Problem Based on the Coarse-grained Model [C]∥Proceedings of the 12th International FLINS Conference on Uncertainty Modelling in Knowledge Engineering and Decision Ma-king.City Council of Roubaix:World Scientific Publishing Co.Pte Ltd,2016:489-495.
[3]陈稳.基于DPLL的SAT算法的研究及应用[D].成都:电子科技大学,2011.
[4]JIANG C,ZHANG T.Partial Backtracking in CDCL Solvers[C]∥ Proceedings of the 19th International Conference on Logic for Programming,Artificial Intelligence,and Reasoning.Berlin Heidelberg:Springer Verlag,2013:490-502.
[5]MARQUESSILVA J P,SAKALLAH K A.GRASP:A Search Algorithm for Propositional Satisfiability[J].IEEE Transactions on Computers,1999,48(5):506-521.
[6]MARQUES SILVA J P,SAKALLAH K A.GRASP—A New Search Algorithm for Satisfiability[C]∥Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design.Digest of Technical Papers:IEEE Press,2003:73-89.
[7]MOSKEWICZ M W,MADIAN C F,ZHAO Y,et al.Chaff:Engineering an Efficient SAT Solver[C]∥Proceedings of the 38th Design Automation Conference.United States:IEEE Press,2005:530-535.
[8]LIANG J H,GANESH V,ZULKOSKI E,et al.Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers[C]∥Proceedings of the 11th International Haifa Verification Conference on Verification and Testing of Hardware and Software.Haifa(Israel):Springer International Publishing,2015:225-241.
[9]DERSHOWITZ N,HANNA Z,NADEL A.A Clause-based Heuristic for SAT Solvers[C]∥Proceedings of the 8th International Conference on Theory and Applications of Satisfiability Testing.Intel Corporation:Springer-Verlag,2005:46-60.
[10]BIERE A,FROHLICH A.Evaluating CDCL Variable Scoring Schemes[C]∥Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing.Bioinformatics:Springer International Publishing,2015:405-422.
[11]CHEN J.A Dynamic Phase Selection Strategy for Satisfiability Solvers [J].Computer Science,2012,13(5):208-213.
[12]CHEN J.Phase Selection Heuristics for Satisfiability Solvers[J].Computer Science,2011,36(6):312-320.
[13]CHEN J.A Bit-Encoding Phase Selection Strategy for Satisfia-bility Solvers[C]∥Proceedings of the 11th Annual Conference on Theory and Applications of Models of Computation.New York:Springer Verlag,2014:158-167.
[14]PIPATSRISAWAT K,DARWICHE A.A Lightweight Comp-onent Caching Scheme for Satisfiability Solvers[C]∥Procee-dings of the 10th International Conference on Theory and Applications of Satisfiability Testing.Lisbon Portugal:Springer Verlag,2007:294-299.
[15]刘志明,吴明芬,许勇.一种基于遗传算法的权重的确定方法 [J].五邑大学学报(自然科学版),2006,20(3):45-48.
[16]LIANG J H,GANESH V,POUPART P,et al.Exponential Recency Weighted Average Branching Heuristic for SAT Solvers[C]∥Proceedings of the 30th AAAI Conference on Artificial Intelligence.Infosys:AAAI Press,2016:3434-3440.
[17]SILVA J,MARQUES O P.The Impact of Branching Heuristics in Propositional Satisfiability Algorithms[C]∥Proceedings of the 9th Portuguese Conference on Artificial Intelligence.Berlin Heidelberg:Springer Verlag,1999:62-74.
[18]LIU Y,WANG J,XU C,et al.An Effective Branching Strategy Based on Structural Relationship among Multiple Forbidden Induced Subgraphs [J].Journal of Combinatorial Optimization,2015,29(1):257-275.

相关文章 15

[1]	周乐员, 张剑华, 袁甜甜, 陈胜勇. 多层注意力机制融合的序列到序列中国连续手语识别和翻译 Sequence-to-Sequence Chinese Continuous Sign Language Recognition and Translation with Multi- layer Attention Mechanism Fusion 计算机科学, 2022, 49(9): 155-161. https://doi.org/10.11896/jsjkx.210800026
[2]	高振卓, 王志海, 刘海洋. 嵌入典型时间序列特征的随机Shapelet森林算法 Random Shapelet Forest Algorithm Embedded with Canonical Time Series Features 计算机科学, 2022, 49(7): 40-49. https://doi.org/10.11896/jsjkx.210700226
[3]	刘宝宝, 杨菁菁, 陶露, 王贺应. 基于DE-LSTM模型的教育统计数据预测研究 Study on Prediction of Educational Statistical Data Based on DE-LSTM Model 计算机科学, 2022, 49(6A): 261-266. https://doi.org/10.11896/jsjkx.220300120
[4]	孙福权, 梁莹. 基于XGBoost算法的水稻基因组6mA位点识别研究 Identification of 6mA Sites in Rice Genome Based on XGBoost Algorithm 计算机科学, 2022, 49(6A): 309-313. https://doi.org/10.11896/jsjkx.210700262
[5]	陈慧嫔, 王琨, 杨恒, 郑智捷. 蓝舌病毒基因组序列多元概率特征可视化分析 Visual Analysis of Multiple Probability Features of Bluetongue Virus Genome Sequence 计算机科学, 2022, 49(6A): 27-31. https://doi.org/10.11896/jsjkx.210300129
[6]	赵耿, 王超, 马英杰. 基于混沌序列相关性的峰均比抑制研究 Study on PAPR Reduction Based on Correlation of Chaotic Sequences 计算机科学, 2022, 49(5): 250-255. https://doi.org/10.11896/jsjkx.210400292
[7]	沈少朋, 马洪江, 张智恒, 周相兵, 朱春满, 温佐承. 多元时序上状态转移模式的三支漂移检测 Three-way Drift Detection for State Transition Pattern on Multivariate Time Series 计算机科学, 2022, 49(4): 144-151. https://doi.org/10.11896/jsjkx.210600045
[8]	赵耿, 李文健, 马英杰. 基于离散动力学反控制的混沌序列密码算法 Chaotic Sequence Cipher Algorithm Based on Discrete Anti-control 计算机科学, 2022, 49(4): 376-384. https://doi.org/10.11896/jsjkx.210300116
[9]	高堰泸, 徐圆, 朱群雄. 基于A-DLSTM夹层网络结构的电能消耗预测方法 Predicting Electric Energy Consumption Using Sandwich Structure of Attention in Double -LSTM 计算机科学, 2022, 49(3): 269-275. https://doi.org/10.11896/jsjkx.210100006
[10]	陈伟, 李杭, 李维华. 核小体定位预测的集成学习方法 Ensemble Learning Method for Nucleosome Localization Prediction 计算机科学, 2022, 49(2): 285-291. https://doi.org/10.11896/jsjkx.201100195
[11]	陈晋鹏, 胡哈蕾, 张帆, 曹源, 孙鹏飞. 融合时间特性和用户偏好的卷积序列化推荐 Convolutional Sequential Recommendation with Temporal Feature and User Preference 计算机科学, 2022, 49(1): 115-120. https://doi.org/10.11896/jsjkx.201200192
[12]	程思伟, 葛唯益, 王羽, 徐建. BGCN:基于BERT和图卷积网络的触发词检测 BGCN:Trigger Detection Based on BERT and Graph Convolution Network 计算机科学, 2021, 48(7): 292-298. https://doi.org/10.11896/jsjkx.200500133
[13]	杨萍, 舒辉, 康绯, 卜文娟, 黄宇垚. 一种基于语义分析的恶意代码攻击图生成方法 Generating Malicious Code Attack Graph Using Semantic Analysis 计算机科学, 2021, 48(6A): 448-458. https://doi.org/10.11896/jsjkx.201100074
[14]	张争万, 吴迪, 张春炯. 基于多通道稀疏LSTM的蜂窝流量预测研究 Study of Cellular Traffic Prediction Based on Multi-channel Sparse LSTM 计算机科学, 2021, 48(6): 296-300. https://doi.org/10.11896/jsjkx.210400134
[15]	黄铭, 孙林夫, 任春华, 吴奇石. 改进KNN的时间序列分析方法 Improved KNN Time Series Analysis Method 计算机科学, 2021, 48(6): 71-78. https://doi.org/10.11896/jsjkx.200500044

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed