Research On Branching Strategy And Deletion Strategy Based On CDCL Solver

SAT problem is a famous problem in computer science theory and artificial intelligence.NP-complete problem(NPC)ranked first in the seven difficult math problems of the millennium,Many NP-complete problems can be solved by converting to SAT problems in polynomial time.The SAT problem is widely used in many fields such as mathematical theorem proving,computer software and theory,engineering technology,software verification,and logic circuit equivalence verification.Therefore,the SAT issue has always been a hot issue for scholars at home and abroad,Efficient algorithms for designing and implementing SAT problems have important implications and application perspectives.The DPLL solver pioneered the solution to the SAT problem,but its algorithm's backtracking mechanism has a certain degree of constraint on the solution of large-scale problems.In order to improve the efficiency of the DPLL algorithm,scholars at home and abroad have done a lot of research and added some key technologies.For example,heuristic branching strategy,based on conflict analysis and clause learnt,non-sequential backtracking,learnt clause deletion and periodic restart,etc.,the most popular CDCL(Conflict-Driven-Clause-Learning,CDCL)solver is formed.Based on the CDCL algorithm structure,this paper has done the following research work:1.Drawing on the idea of VSIDS strategy and its extension strategy,we study the influence of the decision-making level of variables and the number of conflicts of variables participating in conflicts on the branch decision-making stage.An improved heuristic branching strategy is proposed--heuristic selection strategy based variable decision level(HSVDL),It provides the basis for branch decisions and guides the search process of the solver.2.After fully considering the length of the clause of the learnt clause and the influence of the decision-making level of the variable on the deletion of the clause,in order to give full play to the advantages of short clauses in the deductive process,the definition of the average clause length is given,and the deletion strategy is used to delete the longer learnt clause.Then a new learning clause deletion strategy is proposed--based on learnt clause length and LBD deletion strategy(LLBD).3.HSVDL strategy and LLBD strategy are respectively formed into corresponding algorithms,which are embedded in the famous solver Glucose4.1,then to get the new solvers Glucose4.1+HSVDL and Glucose4.1+LLBD.Moreover,HSVDL strategy and LLBD strategy are simultaneously embedded in the solver Glucose4.1 to get a new solver Glucose4.1+HSVDL+LLBD.The competition examples of the 2017 and 2018 SAT International Competitions were selected for testing.The test results are compared with the test results of the solver Glucose4.1 from the number of successful solves,the average number of decision times,the average number of conflicts,the average number of restarts and the average time,The result indicates that the effectiveness and advantages of the solver.