Local Search Based On Probabilistic Reasoning For SAT Problems

As a classical problem in the field of computer science and theory,the Boolean Satisfiability Problem(SAT)has a wide range of application prospsects,and is also a hot topic in current academic research.The SAT resolvers mainly include complete algorithms and incomplete algorithms.Among incomplete algorithms,the algorithm of SLS(Stochastic Local Search)attract a wide spread attention and researches due to its efficiency.However,one shortcoming of SLS is that it is easily get trapped in local minima during the search process,and is particularly evident when solving structured benchmarks,so how to avoid local minimas effectively is the key to improve solving efficiency.This paper statisticed and analyzed the historical search trajectory,explored the complex relationships between variable and clause during the local search,thus proposed a probability reasoning model of computting the probability of making a clause satisfied or unsatisfied by flipping a variable indirectly.Using it computes the probability of making clauses unsatisfied based on the model after a variable is chosen for flipping,thus formed a new taboo strategy of variable—SLPR(Statistic Learning and Probabilistic Reasoning)based on probabilistic reasoning.Through replace the break-tie mechanism of gNovelty+ by the this new taboo strategy of variable and an improved algorithm—gNovelty+SLPR was designed.We contrasted gNovelty+SLPR with gNovelty+ and gNovelty+PCL by comparing the steps and local minimas in solving random and structured benchmarks.Experiment results shows that comparing to gNovelty+ and gNovelty+PCL,gNovelty+SLPR got less steps and local minimas in most case on structured benchmarks,advantage is obvious.For random benchmarks especially large random cases,the number of flip steps and local minimas is also reduced to a certain extend.