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

Back-jump levels based learnt clauses deletion strategy for SAT solver

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

At present,the widely used method for learnt clauses deletion strategy is based on the LBD evaluation method,which deletes the learnt clauses with the first half of the LBD value in each deletion operation.For the large LBD value,this method is too aggressive.To solve this problem,this paper proposed an evaluation method that used back-jump levels to preserve the relevant learnt clauses with large LBD value.Based on the CDCL complete algorithm,it formed the BJL deletion algorithm in the learnt clauses deletion stage.It conducted a comparative experiment on the newly improved version and the original version by testing the 2017 SAT international competition.Experiments show that the proposed strategy can significantly improve the solver’s performance and efficiency.