基于动态奖惩的CDCL SAT求解器分支启发式算法

• 作者: 刘婷 陈秀兰
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: SAT问题 分支启发式算法 VSIDS 决策层 冲突决策层 变量冲突频率
• 年，卷（期）: 2019,（3）
• 所属期刊栏目: 软件工程
• 页码范围: 490-497
• 页数: 8页
• 分类号: TP181
• 字数: 6821字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2019.03.015

摘要

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响.为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法.每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分.用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例.实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘婷	西南交通大学系统可信性自动验证国家地方联合工程实验室	9	49	3.0	7.0
2	陈秀兰	西南交通大学系统可信性自动验证国家地方联合工程实验室	2	0	0.0	0.0