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

来源：计算机应用研究杂志2020年第11期北京时间：

作者：沈雪,陈树伟,徐扬,吴贯锋,

单位：1.西南交通大学a.数学学院;b.信息科学与技术学院,成都610031；2.系统可信性自动验证国家地方联合工程实验室,成都610031；

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

关键词：可满足性问题,冲突驱动子句学习,LBD,回跳层数,

基金资助：国家自然科学基金资助项目(61673320)；中央高校基本科研业务费专项资金资助项目(2682018ZT10,2682018CX59)；；