基于变量混合特征的分支启发式策略

先进的SAT求解器能够通过有效的分支启发式策略解决大型应用实例.目前VSIDS策略是最具有代表性的基于冲突分析的分支策略，它因其稳健性而被广泛使用，但在每次冲突分析中其判定变量活性的增量方式过于单一.针对此问题，本文提出了一种基于变量混合特征的分支启发式算法，目的是充分地利用参与冲突分析的变量所携带的不同信息特征来区分变量，来进一步指导变量活性增长.并将所提出的分支策略算法嵌入到Glucose4.1中形成求解器Glucose4.1+MFBS，通过对比测试，实验结果表明改进的分支算法比原本的VSIDS策略，具有一定的优势，求解明显个数增加.

Branching Heuristic Strategy Based on Variable Mixing Features

Advanced SAT solvers solve large application instances with efficient branching heuristics. At present, the VSIDS strategy is the most representative branching strategy based on conflict analysis. It is widely used because of its robustness. However, in each conflict analysis, the incremental method of determining the variable activity is too single. To solve this problem, this study proposes a branch heuristic algorithm based on variable mixing features. The purpose is to fully utilize the different information features carried in the variables involved in conflict analysis to distinguish variables, and further guide the variable activity growth. The proposed branching strategy algorithm is embedded into Glucose4.1 to form the solver Glucose4.1+MFBS. Through experimental comparison and analysis, the experimental results show that the improved branching algorithm has certain advantages over the original VSIDS strategy, and the number of solutions increases obviously.