Abstract: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.