Research On Variable Decision Algorithm Based On CDCL Learning Framework

The Boolean Satisfiability Problem(SAT)is a central Problem in the fields of artificial intelligence,mathematical logic,computer science and so on.Since 1971,American computer scientist Stephen Cook first proved that SAT problem is nondeterministic Polynomial Complete(NPC)problem by using the theoretical concept of Turing machine,SAT problem has been attracting much attention.Since one NPC problem can be transformed into another NPC problem in polynomial time and all NPC problems are computed in the same way,SAT problem can be used as a starting point for all NPC problems.If a high-performance SAT solving algorithm can be designed to solve SAT problems in polynomial time.Then all NPC problems can be solved in polynomial time,so it can be proved that NP=P.Many scholars try to find a new efficient algorithm for solving SAT problems.At present,it is still of great significance to design a powerful algorithm for solving SAT problems.According to the completeness,there are two kinds of algorithms for solving SAT problems: complete algorithm and incomplete algorithm.Although the time complexity of the incomplete algorithm is polynomial and it is better than the complete algorithm in solving speed,the incomplete algorithm cannot guarantee that it can find the solution of the corresponding problem.Although the complete algorithm can theoretically give the solution of all the satisfiable problems,and can directly prove the unsatisfiable problems,the time complexity of the complete algorithm is at the highest exponent level,and the binary tree search space should be exhausted in theory to find the solution of the problem.In practical application,for a given problem,when the problem is satisfiable,the solver needs to give the corresponding satisfiable solution,and when the problem is unsatisfiable,it needs to give a complete proof.Therefore,the main research work in this paper is carried out on the basis of complete algorithm.In this paper,based on the mainstream complete algorithm-Conflict Driven Cluster-Learning SAT(CDCL-SAT)solution framework,the variable decision strategy is improved with the goal of improving the solver performance.Early variable decision making strategies all rely on some inherent characteristics of clauses,such as the number of clauses,clause length,the number of unassigned variables as the characteristic parameters of decision variables.At present,most of the mainstream variable decision strategies are variable evaluation based on conflicts.Aiming at the shortcomings of the above variable decision strategies,the conjecture that the deletion of learning clauses will affect Boolean Constraint Propagation(BCP)is proposed.The original code of solver was improved to extract the number of clauses in which variables were found before and after the deletion of learning clauses,and the conjecture was confirmed by design experiments.Given that these policies do not take into account the impact of the number of clauses in which the decision variable resides on the BCP,Variable Decision Algorithm Based on learning clause Deletion(VDALCD)was proposed,and the calculation method of Variable activity was improved.Embed the VDALCD policy into the solver for Glucose4.1,Maple LCMDist Chrono BT-DL-v2.1 and Relaxed?LCMDCBDL?new Tech.The improved solver is defined as glucose4.1?VDALCD,Maple-DL?VDALCD and RLNT?VDALCD,respectively.Taking the example of the Main group of 2018 SAT competition as the test benchmark,glucose4.1?vdalcd solved 26 more examples than the original solver Glucose4.1,an increase of 15.5%.Taking the Main group example of 2019 SAT competition as the test benchmark,Maple-DL?VDALCD solved 17 more examples than the original solver Maple LCMDist Chrono BT-DL-v2.1,an increase of7.6%.Six more examples were solved than 2019 champion solver Ca Di Cal,an increase of 3.1%.For random class problems,the improved RLNT?VDALCD solver is 82 more than the original solver,an increase of 12.8%.Compared with the champion solver Kissat?sc2020?sat in 2020,442 more are solved,an increase of 158.9%.Therefore,the VDALCD algorithm proposed in this paper can effectively improve the performance of the SAT solver.