Research On Solving Algorithm Of SAT Problem Based On Branching Strategy And Distance Ratio Deletion Strategy

Many problems in natural science and social science can be transformed into Satisfiability Problem,which is also one of the core problems in computer and artificial intelligence.Therefore,with the rapid development of computer science and intelligent information,it is significance to study SAT and its solution in order to solve various practical problems.Algorithms in SAT problems are mainly divided into complete algorithm and incomplete algorithm.This paper mainly studies CDCL(Conflict Drive Clause Learning)algorithm in complete algorithm.In the basic solving process of CDCL algorithm,branching process and clause learning process are two very important stages,which have great influence on the solving efficiency and solving speed.However,most of the improved algorithms fail to consider other stages of the whole algorithm in the branch process,so the solution result is not optimal.Based on this,this paper considers the impact of the conflict analysis stage on the branching process,combines the impact of the two stages of backtracking and restart,and proposes an improved branching strategy for the decision-making level of weighted decision variables.The new strategy designs a new scoring function of variables,which has the advantage of faster selection of decision variables in the branching process,so as to reduce the subsequent conflicts and restart times,and finally reduce the solution time.The experimental results show that the new branch strategy has optimization effect.In addition,most algorithms now learning process assessment in clause clause quality is to study the length,activity or literal block distance(LBD)of the learning clause as the evaluation standard,but there are few considering new delete standards,based on this,this article consider balance LBD value and puts forward the concept of literal block close combined with the activity of learning clauses,and puts forward the learning clauses deletion strategy based on distance ratio.The new strategy can delete the learning clauses with low utilization rate more effectively,so as to strengthen the solver's solving ability,increase the number of solving examples and reduce the solving time.The experimental results show that the new strategy has better solving ability.The main research work of this paper is as follows:1.By analyzing the process of conflict,backtracking and restart,according to the times of variables as decision variable and its decision level,a new variable score calculation function method is proposed,and then the weighted decision variable level(DVT)strategy is proposed,and the DVT strategy is embedded in the CDCL to form the Glucose4.1+DVT solver.The basic examples of SATLIB and the test examples of the Main Track group of the international SAT competition in 2019,2018 and 2017 is used for the experimental test.The results show that the average total time of the new solver's successful solution is 10% shorter than that of the original solver,and the total number of successfully solved test cases is 6more than that of the original solver.2.As a large number of learning clauses are generated in the learning process of conflict clauses,the concept of literal block close and the learning clause deletion strategy(LBDR)of the distance ratio are proposed based on the idea of equilibrium LBD value,and the strategy is added into the CDCL algorithm to form the Glucose4.1+LBDR solver.The basic examples of SATLIB and the test examples of the Main Track group of the international SAT competition in 2019,2018 and 2017 are adopted for the experimental test.The results show that the successful solution time of the new solver is 12.5% shorter than that of the original solver,and the total number of examples successfully solved is 14 more than that of the original solver.