基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句，避免学习子句规模呈几何级增长，减少冗余学习子句对系统内存占用，从而提高布尔可满足性问题SAT求解器的求解效率，需要对学习子句进行评估，然后删减学习子句。传统的评估方式是基于学习子句的长度，保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式，另外一个是基于文字块距离LBD的评估方式，也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析，将学习子句使用频率与LBD评估算法混合使用，既反映了学习子句在冲突分析中的作用，也充分利用了文字与决策层之间的信息。以Syrup求解器（GLUCOSE 4.1并行版本）为基准，在评估算法与并行子句共享策略方面做改进测试，通过实验对比发现，混合评估算法比LBD评估算法有优势，求解问题个数明显增多。

A hybrid learnt clause evaluation algorithmfor SAT problem based on frequency

In order to effectively manage learnt clauses, avoid a geometrical growth of their scale, reduce the memory cost of redundant learnt clauses and improve the efficiency of the Boolean satisfiability problem (SAT) solver, we need to evaluate learnt clauses and delete some redundant ones. Traditional evaluation methods are based on the length of learnt clauses, and short-length ones are kept. Two current mainstream clause evaluation methods are the variable state independent decaying sum (VSIDS), and a method based on the evaluation of the literals blocks distance (LBD), and the combination of the above two is also used as the basis for clause evaluation. We analyze the relationship between the number of learnt clauses used in conflict analysis and problem solving, and combine the frequency of learnt clauses with the LBD evaluation algorithm, which not only reflects the role of learnt clauses in conflict analysis, but also makes full use of the information between text and decision-making layer. Taking the Syrup solver (GLUCOSE 4.1 parallel version) as baseline, experiments are carried out to evaluate the algorithm and the parallel clause sharing strategy. The experimental comparison shows that the the proposed hybrid evaluation algorithm outperforms the LBD evaluation algorithm, and the number of solving problems is significantly increased.