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

• 作者: 吴贯锋 徐扬 沈雪 陈树伟
• 来源期刊: 计算机应用研究
• 关键词: 可满足性问题 冲突驱动子句学习 LBD 回跳层数
• 年，卷（期）: 2020,（11）
• 所属期刊栏目: 算法研究探讨
• 页码范围: 3316-3320
• 页数: 5页
• 分类号: TP391
• 语种: 中文
• DOI: 10.19734/j.issn.1001-3695.2019.07.0269

摘要

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