《计算机应用研究》|Application Research of Computers

基于参与冲突分析次数的动态学习子句评估策略

Dynamic learnt clause evaluation strategy based on number of participations in conflict analysis

免费全文下载 (已被下载 次)  
获取PDF全文
作者 孙菁,钟小梅,徐扬
机构 1.西南交通大学 数学学院,成都 610031;2.系统可信性自动验证国家地方联合工程实验室,成都 610031
统计 摘要被查看 次,已被下载
文章编号 1001-3695(2020)10-004-2902-05
DOI 10.19734/j.issn.1001-3695.2019.06.0205
摘要 针对现有学习子句评估策略的单一性,提出一种基于学习子句参与冲突分析次数的评估策略,并将该策略分别与经典的文字块距离评估策略和活跃值评估策略结合,形成两个动态学习子句评估策略。基于2018年SAT国际竞赛部分基准实例,将动态评估策略与原评估策略进行参数适应性对比实验,并通过2018和2017年的基准实例进行评估。结果表明动态评估策略能更好地评估学习子句的质量,由此生成的求解器在求解数量和速度方面表现出较好的求解性能。
关键词 可满足性问题; 冲突分析; 学习子句评估; 学习子句删除
基金项目 国家自然科学基金资助项目(61673320)
本文URL http://www.arocmag.com/article/01-2020-10-004.html
英文标题 Dynamic learnt clause evaluation strategy based on number of participations in conflict analysis
作者英文名 Sun Jing, Zhong Xiaomei, Xu Yang
机构英文名 1.School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China;2.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,Chengdu 610031,China
英文摘要 Avoiding the singularity of the existing learnt clause strategies, this paper proposed a new learnt clause evaluation strategy based on the number of participations in conflict analysis, and then combined with literals blocks distance(LBD) evaluation strategy and activity evaluation strategy respectively forming two dynamic evaluation strategies. Then, using partial SAT international benchmark instances in 2018, this paper compared solvers results under new strategies(i. e., two dynamic evaluation strategies) with original ones(i. e., literals blocks distance(LBD) evaluation strategy and activity evaluation strategy). And, it conducted evaluation experiments through benchmark instances in 2018 and 2017. The experimental results show that the dynamic evaluation strategy can preferably estimate the quality of learnt clauses and the solver based on new strategy has better solving performance in the number and speed.
英文关键词 satisfiability problem; conflict analysis; learnt clause evaluation; learnt clause reduction
参考文献 查看稿件参考文献
 
收稿日期 2019/6/27
修回日期 2019/8/5
页码 2902-2906
中图分类号 TP301.6
文献标志码 A