关键词: 冲突驱动子句学习, 分支策略, 回溯搜索, 可满足性问题, 完备算法

Abstract: Branching decision is one of the most critical parts of CDCL solver,and an excellent branching strategy can reduce the number of branching decisions and improve the SAT solver’s efficiency.Most of the state-of-art branching strategies have incorporated the conflict analysis process.But the branching strategies have different reward methods on variables participating in conflict analysis,so the selected branching variables are different.In this paper,considering the important fact that decision variables are always selected in the unassigned variable set,a new branching strategy based on the EVSIDS (Exponential Variable State Independent Decaying Sum) branching strategy is proposed,which is called the branching strategy based on the reward mechanism (referred to as the RACT branching strategy).The RACT branching strategy is to reward the variables that are de-assigned in the conflict analysis again to increase the probability that the variables that are frequently involved in the conflict analysis in the unassigned variables are selected as branch variables.Finally,the proposed branching strategy is embedded into the Glucose4.1 solver to form a new solver Glucose4.1+RACT,and the effectiveness of the RACT branching strategy is tested by using 350 instances of the 2017 SAT competition as experimental data sets.The experimental comparison shows that the solver Glucose4.1+RACT can solve more instances than the original solver,especially with an increase of 13.5% in the number of satisfied instances,and the total time spent on solving 350 competition examples is also 3.9% lower than that of Glucose 4.1.The above experimental data shows that the proposed branching strategy can effectively reduce the number of branch decisions in the search tree and give the correct search space,thus improving the solving ability of the SAT solver.

Key words: Backtrack search, Branching strategy, Complete algorithms, Conflict driven clause learning, Satisfiability problem