Study On Local Search For Random Satisfiability

Satisfiability Problem(SAT)in propositional logic is a fundamental problem in computer science theory and practice.SAT problem lies in determining whether a given formula can be satisfied by an assignment to its Boolean variables.In theoretical aspects,SAT solver has been applied to combinatorial optimization,statistical physics,computing theory and other fields.In practical application,SAT solver has been applied to computer algebra systems,core graphs,gene regulatory networks,automated system(software/hardware)verification,circuit verification,model-based diagnosis,and machine induction etc.Therefore,research on efficient algorithms for solving SAT problems has important theoretical significance and application value.Algorithms for solving SAT problems are mainly divided into two categories: complete algorithms and incomplete algorithms.Stochastic local search(SLS)is one of the most important incomplete algorithms,and many breakthrough incomplete algorithms are based on SLS algorithms.This research of dissertation is focused on the SLS algorithms,and proposes new strategies in initial assignment,variable selection,and clause selection.Based on these strategies,different versions of SLS solvers have been developed.Through experimental evaluation,the different versions of SLS solvers developed are compared with similar solvers and the available state-of-the-art solvers.The results show the obvious superiority of the proposed solvers.In particular,the comparative analysis based on the benchmarks from random track of previous SAT competitions as the test cases further prove the advanced nature of the SLS solvers developed based on a series of new methods and strategies.In the aspect of the initial assignment strategy of the SLS algorithm,by analyzing the inherent properties of SAT problems,the allocation strategy,Satisfaction degree(Sd)and the initial probability distribution are proposed,which can effectively optimize the search direction of the SLS solvers.Based on large-scale experiments,this dissertation analyzes that the allocation strategy based on the initial probability distribution is effective for improving the performance of the SLS solvers on the uniform random k-SAT(URS)problems.In the aspect of the variable selection strategy of the SLS algorithm,by analyzing the search trajectory of the Walk SATlm solver for solving the URS problems,a new strategy(based on the fitting function Boltamann)is proposed to simulate the search behavior of the solver.The probability selection strategy based on Boltamann function is studied.By analyzing the existing the polynomial function and exponential function used in the variable selection strategy of the current SLS solvers based on probability selection,three effective variable selection strategy based the probability are proposed,which are called the variable selection strategy based on the pseudo normal function,the variable selection strategy based on the pseudo normal-polynomial,and the variable selection strategy based on the polynomial-pseudo normal function,which effectively optimize the path search of SLS based on the probability selection.Based on large-scale experiments,this dissertation analyzes that the effectiveness of different variable selection strategies in the SLS solver based on probability selection.The sources of SAT problem are rather diverse and wide,and the solving efficiency of the same SAT algorithm generally differs greatly in different types of SAT instances.Internationally,the state-of-the-art SLS solvers for solving URS problems have no advantages in hard random SAT problems(HRS).In the aspect of the clause selection strategy of the SLS algorithm,in order to tend to choose unsatisfiable clauses that frequently become unsatisfied or easy to remain satisfiable during the search process,two schemes of important factor allocation and a second-level biased random walk strategy are proposed.In the aspect of the variable selection strategy of the SLS algorithm,a new liner scoring function is developed to evaluate different variables.The clause selection strategy and variable selection strategy lead to a new SLS algorithm,named BRSAP,the algorithm's performance in solving HRS problems surpasses the winners in the random track of SAT competitions in 2016,2017 and 2018,and can also effectively solve URS problems with long clauses.The heuristic strategy based on emphasizing flipped variables is studied.By analyzing the search decision in the SLS solving process,a biased random walk strategy with emphasis on the flipping variables and a tie-breaking strategy with emphasis on the flipping variables are proposed,and all these strategies utilized to improve the Prob SAT algorithm lead to a new SLS algorithm named EPEFV.The performance of EPEFV is then evaluated and compared with the state-of-the-art SLS solvers and complete solvers on HRS problems and URS problems with long clauses.Experimental results show that the performance of EPEFV is better than the winners in the random track of the SAT competitions in 2017 and 2018 as well as the winners in the main track of the SAT competitions in 2018 and 2019.The heuristic strategy based on selection attributes is studied.In the aspect of the caluse selection strategy of the SLS algorithm,a new scheme of clause important factor allocation and a new biased random walk strategy are proposed.In the aspect of the variable selection strategy of the SLS algorithm,a new scheme of variable important factor allocation and a variant of Configuration Checking(CC)strategy are designed.These strategies are developed to a new SLS algorithm(named Select NTS)based on the selection attributes.The performance of Select NTS is evaluated and compared with the state-of-the-art SLS solvers and complete solvers on HRS problems and URS problems.Experimental results show that the performance of Select NTS outperforms the winners of the random track of the SAT competitions in 2016,2017,and 2018.The main differences between Select NTS,EPEFV and BRSAP are discussed: Select NTS has established the state-of-the-art standards on HRS problems,EPEFV has better performance than BRSAP on HRS problems,and Select NTS,EPEFV and BRSAP have their own advantages on different types of URS problems.Finally,the relationship between different properties in these three solvers is analyzed theoretically and experimentally.