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