基于学习子句长度和LBD的删除策略

Deletion Strategy Based on Learning Clause Length and LBD

学习子句的删除在求解器的构成中是非常重要的。因为学习子句删除策略的"优劣"不仅影响BCP的效率,还影响内存的占用问题,为避免出现这些问题,很多学者做了大量的工作,提出了很多良好的学习子句删除策略。然而当前的学习子句删除策略都有一个缺点:删除学习子句时有可能会删除在后续搜索过程中有很大作用的子句,因为不能确保每次删除的都是没有"价值"的子句。在充分考虑学习子句的长度和变量的决策层的基础上,本文提出基于学习子句长度和LBD的删除策略——LLBD策略,并形成算法,然后用该策略替换Glucose求解器中的删除策略,最后通过实验表明LLBD策略能够求解出更多的实例,求解器的效率也有所提高,表明本文策略有一定的优势。

The deletion of the learning clause is very important in the composition of solver. The “good or bad” of the learning clause deletion strategy not only affects the efficiency of the BCP, but also affects the memory occupation. In order to avoid these problems, many scholars have done a lot of work and put forward a lot of good learning clause deletion strategies. However, the current learning clause deletion strategy has a disadvantage: it is possible that there is a great effect in the subsequent search process when deleting the learning clause, because we cannot guarantee that the clause that we delete each time has no “value”. Based on the length of learning clause and the decision-making layer of variable, this paper proposes a deletion strategy based on learning clause length and LBD-LLBD strategy. Then, the proposed strategy is embedded in the famous solver Glucose. Finally, experiments show that the proposed strategy can solve more examples. The efficiency of the solver is also improved, indicating that the strategy has certain advantages.