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

Dynamic learnt clause evaluation strategy based on number of participations in conflict analysis

针对现有学习子句评估策略的单一性,提出一种基于学习子句参与冲突分析次数的评估策略,并将该策略分别与经典的文字块距离评估策略和活跃值评估策略结合,形成两个动态学习子句评估策略。基于2018年SAT国际竞赛部分基准实例,将动态评估策略与原评估策略进行参数适应性对比实验,并通过2018和2017年的基准实例进行评估。结果表明动态评估策略能更好地评估学习子句的质量,由此生成的求解器在求解数量和速度方面表现出较好的求解性能。

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.