基于参与冲突分析次数的动态学习子句评估策略.

Avoiding the singularity of the existing learnt clause strategies, this paper proposed a new learnt clause evaluation strategy based on the number of participations in conflict analysis, and then combined with literals blocks distance ( LBD) evaluation strategy and activity evaluation strategy respectively forming two dynamic evaluation strategies. Then, using partial SAT international benchmark instances in 2018, this paper compared solvers results under new strategies ( i. e., two dynamic evaluation strategies) with original ones ( i. e., literals blocks distance ( LBD) evaluation strategy and activity evaluation strategy). And, it conducted evaluation experiments through benchmark instances in 2018 and 2017. The experimental results show that the dynamic evaluation strategy can preferably estimate the quality of learnt clauses and the solver based on new strategy has better solving performance in the number and speed. [ABSTRACT FROM AUTHOR]