Statistical Relational Learning And Probabilistic Inference Technology Of Local Search Algorithm Behavior For Solving SAT Problems

Local search algorithms as the heuristic algorithms,are more efficient algorithm for solving SAT problems,but they have poor efficiency generally in solving structural benchmarks.At present,most local search strategies only consider the simple relational model between variables and clauses.However,there are implicit multivariate relational models in structured SAT benchmarks and difficult random SAT benchmarks,which cause the local Search to be in trouble.Exploring and applying the implicit multivariate relational models between variables and clauses in the SAT local search process by the statistical learning and probability inference technique,brings a new opportunity for SAT problem Solution.In the thesis,we used the classical SAT local search algorithm to solve all kinds of difficult SAT benchmarks,and discussed the relationship events in the process of local search by statistics and analysis,the relationships event models between variables and clauses with structured information were explored.In order to use the learned probability information between relationship events,the sum of the weights of indirectly broken clauses and IBWsat algorithm based on statistical learning and probabilistic inference were proposed.IBWsat algorithm retains the efficient solving efficiency to solve the random benchmarks,and improves the ability to solve structured benchmarks via using the structured information displayed in local search.By comparing the IBWsat algorithm,the probsat algorithm and the efficient WalkSAT algorithm,the experimental results show that the CBWsat algorithm has fewer search steps and solves more benchmarks instances,when solving the structured benchmarks,And It has the efficient search feature as same as the WalkSAT algorithm,and has the good performance of solving as same as probsat algorithm when solving the random benchmarks.