基于动态奖惩的CDCL SAT求解器分支启发式算法

分支启发式算法在CDCL SAT求解器中有着非常重要的作用,传统的分支启发式算法在计算变量活性得分时只考虑了冲突次数而并未考虑决策层和冲突决策层所带来的影响。为了提高SAT问题的求解效率,受EVSIDS和ACIDS的启发,提出了基于动态奖惩DRPB的分支启发式算法。每当冲突发生时,DRPB通过综合考虑冲突次数、决策层、冲突决策层和变量冲突频率来更新变量活性得分。用DRPB替代VSIDS算法改进了Glucose 3.0,并测试了SATLIB基准库、2015年和2016年SAT竞赛中的实例。实验结果表明,与传统、单一的奖励变量分支策略相比,所提分支策略可以通过减少搜索树的分支和布尔约束传播次数来减小搜索树的规模并提高SAT求解器的性能。

A dynamic reward and punishment based branching heuristic algorithm for CDCL SAT solvers

Branching heuristic algorithms play an important role in CDCL SAT solvers, and the conventional branching heuristic algorithms are more concerned with the number of conflicts when calculating the activity scores of variables and do not consider the influence of the decision level or conflict decision level. In order to improve the efficiency of solving SAT problem, we propose a dynamic reward and punishment based branching method (DRPB), which is inspired by the EVSIDS and ACIDS. Whenever a conflict occurs, the DRPB updates the activity score of variables by integrating the numbers of conflicts, decision-making level, conflict decision level, and conflict frequency of variables. We improve the Glucose version 3.0 by replacing the VSIDS algorithm with the DRPB, and conduct an empirical evaluation not only on instances of SATLIB benchmarks, but also on 2015 and 2016 SAT competitions. Experimental results show that compared with the traditional and single variable branching heuristic algorithms, the proposed strategy can reduce the size of the search tree and improve the performance of the SAT solvers by reducing the branches of the search tree and the number of Boolean constraint propagation.