Comprehensive Analysis Of Restart Strategies Of CDCL SAT Algorithm

SAT solvers based on CDCL(Conflict Driven Clause Learning)have been widely used in formal verification.A large number of NP problems in practical application have been proved to be converted into SAT problems,therefore,the efficiency of SAT algorithms have attracted much attention.Many solvers have been widely used in industry.It is used to choose default settings in view of numerous restart strategies and parameters,which leads to reduction of efficiency and ease of use.In order to improve the practicability of CDCL solvers,this thesis experiments on the restarting strategies of the SAT solver based on CDCL algorithms.The thesis originates from Natinal Natural Fund project,and the main work of this thesis is as follows:First,this thesis researches on the development of SAT problem,in depth analysis of the advantages and disadvantages of representative CDCL algorithms,including the DP(Davis-Putnam)algorithm,DPLL(Davis Putnam Logemann Loveland)algorithm,GRASP(Genetic Search Algorithm for the SAT Problem)algorithm,Chaff algorithm,BerkMin(Berkeley-Minsk)algorithm and Glucose algorithm,also the breakthrough technologies of typical solvers.Second,this thesis analyzes how the restart strategies,restart schedules,restart interval increase factors effect solving performance,and the relationship between initial feature sets and restart strategy sets.Last,on the basis of the research that how restart strategies effect solving efficiency,less restart strategies can cover most of the optimal strategies.Therefore,by observing the solver's behaviour at the start of search,the relationship between the change frequency of the initial features and the corresponding restart strategy sets is analyzed.Results demonstrate that the solving distance between the optimal solution and default solving performance is great,and the gap between the optimal solution and the default solving performance can reach 441%,on average;Great individual differences and certain group differences on choosing restart strategies are shown;Compared to restart frequency,restart schedule plays a greater role in solving performance;Changing the restart strategy can improve the solving performance.Comprehensive analysis,there is more room for the satisfiable problem.In addition,seven restart strategies can cover 97% of the optimal strategies.The correlation between the change frequency of the features and the seven strategies provides technical support for choosing the optimal restart strategy.