基于演绎长度的学习子句删除策略

• 作者: 吴贯锋 常文静 徐扬
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 可满足性问题 冲突驱动子句学习 学习子句删除 演绎长度
• 年，卷（期）: 2018,（16）
• 所属期刊栏目: 热点与综述
• 页码范围: 30-36
• 页数: 7页
• 分类号: TP311.1
• 字数: 5964字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1805-0439

摘要

学习子句删除策略是CDCL-SAT求解器中的一个重要内容,可以避免内存爆炸和加速单元传播.评估学习子句有用性的标准不同导致所删除的学习子句是不同的,极大地影响求解效率.基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程,基于此,提出一种基于演绎长度的学习子句评估方法,并与现有的基于文字块距离的评估方法结合,根据排序子句的基准不同,形成两种不同的结合算法.采用国际SAT竞赛的基准实例,与目前主流的求解器进行了实验对比分析.结果表明,所提的结合算法能更好地评估学习子句的有用性,较基于文字块距离策略的求解个数提高了4.1％,说明所提策略具有一定的优势.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学数学学院	186	1462	15.0	32.0
3	常文静	西南交通大学信息科学与技术学院	3	4	1.0	2.0
9	吴贯锋	西南交通大学信息科学与技术学院	4	4	1.0	2.0