Clause Simplification Of Complete Algorithms For Satisfiability Problem

The satisfiability problem(SAT)is a decision problem.And it is applied to determine whether there is a set of truth assignments such that the conjunctive normal form(CNF)is satisfied when a CNF is given.As the first proven nondeterministic polynomial complete(NPC)problem,SAT plays an important role in theoretical research and practical application.Modern SAT complete algorithms are mainly based on the conflict driven clause learning(CDCL)method,which precisely learns the conflicts generated in the searching process for further direction of the searching process.The CDCL SAT solver will generate a large number of learnt clauses during the search process,and both the original clause and the newly generated learnt clause may contain lots of redundant literals.These redundant literals can significantly degrade solving efficiency.In order to improve the solving efficiency of the CDCL SAT solver,we will take clause simplification as the main thread that running through this paper,and we proposes three methods to conduct on three problems currently faced.The main work and contributions are summarized as follows.To solve the problem of the current learning clause simplification technology based on unit propagation,that is,the number of clauses simplified by this technology is small and the time cost is high,a new efficient online learnt clause minimization method based on unit propagation is proposed,called LCM(Learnt Clause Minimization).In this paper,considering the properties of CDCL SAT solver and using heuristic strategy,the simplification timing is firstly optimized,that is,the simplification operation is selected at some restarts during the search process of the solver,then the frequency of simplification operation is gradually reduced through out the progress of the search process.Then,the simplification object needs to be optimized,that is,only those clauses with relatively high quality would be selected for simplification.Finally,the optimization selection is made for the simplification order,that is,unit propagation was performed one by one according to the current order of literals in the clause.Through experiments,we could see that the LCM simplification method can significantly improve the simplification effect,calculation speed and solutions of the CDCL SAT solver.Applying the LCM simplification method to Maple＿LRB,the top solver in the 2016 SAT contest,allowed the solver to solve 15 more examples than Maple＿LRB,which only solved 4 more instances than the fourth place solver.To solve the problem of being expensive to perform comprehensive and in-depth online simplification of all clauses,two simplification methods of learnt clauses and original clauses based on the quality of clauses are proposed incrementally.Firstly,based on the change of value of Literal Block Distance(LBD)in the clause during the search process,the criterion for resimplification of the clause is established,and the Clause Minimization based on LBD(CML)approach is proposed.Then,the criterion that the clause is suitable to be simplified is formulated based on the condition that the clause participates in ”Effective Conflict”,and the Clause Minimization based on LBD and Conflict(CMLC)method is proposed.By running1450 instances from SAT competition in 2014,2016 and 2017,we found that Maple＿CML,the solver based on CML method,solved 34 more instances than Maple＿LCM,the solver based on LCM method.By running a total of 800 instances from SAT competitions in 2018 and 2020,it is found that the solver Maple＿CMLC based on the CMLC method solves 24 more instances than the solver Maple＿CML based on the CML method.To solve the problem that it is difficult to select an appropriate branching strategy for solving specific types of instances,a branching strategy selection method based on the simplification ratio of learnt clauses(redundant literals deletion rate)is proposed,which is called Branching Strategy Selection(BSS).This method can select an effective branching strategy for specific problem types,that is,for the instance with low LCM learnt simplification ratio,we will increase the using frequency of Learning Rate Branching(LRB)to improve the solving performance.All instances from SAT competition in 2017,2018 and 2020 are tested and it is found that the BSS approach could significantly improve the solver’s performance.Especially for instances in SAT competition 2020,the BSS method could optimize Maple＿CML to solve16 more instances.The relevant work has also been proved in official international competitions:Maple＿LCM and Maple＿CML,solvers based on LCM and CML,won the first and third place in the Main track of SAT Competition 2017 and 2018 respectively.