Research On Branching And Clause Deletion Strategies Based On Backtracking For SAT Algorithm

The satisfiability problem(SAT problem)is a classic decision problem in logic and has also proved to be an NPC(Non-deterministic Polynomial Complete)problem.Since NPC problems can be converted into each other in polynomial time,all NPC problems can be converted to SAT problems for solution.In addition,in practical applications,many problems in areas such as computer-aided design and manufacturing,bioinformatics,artificial intelligence,etc.can be converted into SAT problems for solution.Therefore,quickly solving the SAT problem has important research value.In recent decades,great progress has been made in the study of SAT problems,especially the proposal of CDCL(Conflict Driven Clause Learning)algorithm,which enables solvers to solve hundreds of thousands of variables and millions of industrial examples of clauses in a few minutes.Therefore,the research work in this paper is mainly based on the CDCL algorithm as the algorithm framework,and systematically researches on branching variable decision-making and learning clause evaluation.Based on the existing methods,a series of improvement strategies and new methods are proposed,and the validity is verified by theoretical analysis and experiments.The main innovations of this article are:1.In order to solve the problem of low branching decision efficiency in solving the SAT problem,this paper proposes two rewards based branching heuristic(TRBH)strategy based on the EVSIDS(Exponential Variable State Independent Decay Sum)branching strategy.Considering that the branching decision variables are selected from the unassigned variable set,for variables that have been converted to an unassigned state during the backtracking period,the TRBH branching strategy combines these variables with the last time they participated in the conflict analysis,and again gives these variables a reward.By the way of the two rewards,the possibility that the variable that has participated in the conflict analysis last time and has not been assigned is selected as the decision variable can be increased,thereby changing the selection rule of the decision variable.2.To solve the problem of low clause utilization caused by the single use of LBD(Literals Blocks Distance)value to evaluate clauses.Based on the LBD evaluation method,this paper adds a learning clause deletion strategy of back-jump levels(BJL).The deletion strategy evaluates the quality of learning clauses by using the number of jump back levels of learning clauses,because the higher the number of jump back levels of learning clauses,the stronger the pruning ability of the binary tree in the search process.In other words,the pruning efficiency can be increased,the search speed can be accelerated,and the solving time of the solver can be reduced.3.The TRBH branching strategy and BJL deletion strategy were embedded into Glucose4.1,respectively,to form solvers Glucose4.1+TRBH and Glucose4.1+BJL,and then the examples of SAT competitions from 2017 to 2019 were experimentally tested.In the branching strategy experiment,the experimental results show that the new branching strategy can effectively reduce the number of branching decisions and improve the efficiency of SAT solver by comparing the number of solutions,average time and decision times of two solvers,Glucose4.1+TRBH and Glucose4.1.In the deletion strategy experiment,the experimental results show that the deletion strategy of BJL is more scientific and reasonable than that of a single LBD.