基于回跳层数的SAT求解器学习子句删除策略

沈雪; 陈树伟; 徐扬; 吴贯锋

首页> 中文期刊> 《计算机应用研究》 >基于回跳层数的SAT求解器学习子句删除策略

基于回跳层数的SAT求解器学习子句删除策略

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进.针对此问题,提出了一种利用冲突回跳层数(back-jump levels)的评估方式来保留LBD值较大的有用学习子句.以CDCL(conflict driven clause learning)完备算法为框架,在子句删除环节形成了BJL删除算法.通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验.实验表明,所提策略可显著提高求解器的求解性能和求解效率.

著录项

来源
《计算机应用研究》 |2020年第11期|3316-3320|共5页
作者
沈雪; 陈树伟; 徐扬; 吴贯锋;
展开▼
作者单位

西南交通大学数学学院成都610031;

系统可信性自动验证国家地方联合工程实验室成都610031;

西南交通大学数学学院成都610031;

系统可信性自动验证国家地方联合工程实验室成都610031;

西南交通大学数学学院成都610031;

系统可信性自动验证国家地方联合工程实验室成都610031;

西南交通大学信息科学与技术学院成都610031;

系统可信性自动验证国家地方联合工程实验室成都610031;

展开▼
原文格式 PDF
正文语种 chi
中图分类信息处理（信息加工）;
关键词
可满足性问题; 冲突驱动子句学习; LBD; 回跳层数;

相似文献

中文文献
外文文献
专利

1. 基于学习子句删除策略的SAT求解器分支策略 [J] . 王钇杰 ,徐扬 ,吴贯锋 . 计算机科学 . 2021,第011期
2. 基于子句的动态检查强制文字的SAT求解器 [J] . 常文静 ,徐扬 . 计算机工程与科学 . 2019,第002期
3. 基于学习子句长度和LBD的删除策略 [J] . 刘姚 ,宋振明 . 计算机与现代化 . 2019,第005期
4. 基于演绎长度的学习子句删除策略 [J] . 常文静 ,徐扬 ,吴贯锋 . 计算机工程与应用 . 2018,第016期
5. 基于频次的SAT问题学习子句混合评估算法 [J] . 吴贯锋 ,徐扬 ,陈青山 . 计算机工程与科学 . 2019,第008期
6. CDCL SAT求解器的重启策略分析 [C] . Cheng Rui ,程睿 ,Zhou Cailan . 2017中国计算机辅助设计与图形学大会（2017 China CADCG） . 2017
7. SAT算法中基于回溯的分支和子句删除策略的研究 [A] . 沈雪 . 2020

基于回跳层数的SAT求解器学习子句删除策略

摘要

著录项

相似文献

相关主题

期刊订阅