关键词: SAT求解器, 学习子句删除, LLBD策略, LBD

Abstract: 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.

Key words: SAT solver, learning clause deletion, LLBD strategy, LBD