关键词: 启发式分支策略, SAT求解器, VSIDS策略, HSVDL策略, 变量决策

Abstract: The heuristic branch strategy is an integral part of the SAT solver and directly affects the efficiency of the solver. Early heuristic branch decisions require traversal of the entire clause database, which is inefficient. With the emergence of variable state independent decaying sum (VSIDS) branch strategy, the efficiency of the SAT solver is improved, but the increments of the variables in the VSIDS strategy and its extended strategy are only related to the number of conflicts with the variable, and do not consider the influence of the decision layer of the variable in the branching strategy. Therefore, when a conflict occurs, if the scores of the variables related to the conflict are the identical but the decision levels are different, the choice of variables is random. Based on this, after expounding the importance of the decision level of variables, based on the VSIDS strategy, a heuristic variable selection strategy named HSVDL strategy based on variable decision level is proposed. Then the example shows that the HSVDL strategy is more likely to choose the variable with lower decision-making level than the variable with higher decision-making level in the variable decision-making stage, and the score is smaller, which reduces the memory occupation. Finally, experiments show that the HSVDL strategy can solve more examples, and the efficiency of the solver is also improved, indicating that the strategy has certain advantages.

Key words: heuristic branch strategy, SAT solver, VSIDS strategy, HSVDL strategy, variable decision