Deep Learning Based Stochastic Local Search Algorithm For SAT Problem

The satisfiability(SAT)problem is one of the most important problems in computer science.Any NP problem can be reduced to a satisfiability problem in polynomial time.Many practical problems,such as planning problems,scheduling problems,combinatorial optimization problems,etc.can be coded as SAT problems and quickly solved by a SAT solver.Stochastic local search algorithms are a class of methods that can solve SAT problems efficiently,and many excellent algorithms have been proposed at home and abroad in recent years.The purpose of this paper is to improve the efficiency of the stochastic local search algorithm by using the information in the data distribution of SAT problems through machine learning.Stochastic local search is essentially the process of continuously searching for locally optimal solutions.First,an initial assignment is used to determine the initial value of the formula variable,and then the local optimal solution is optimized by flipping the variable of the formula until a solution is found.In this paper,these two main steps of stochastic local search are improved separately.First,this paper proposes a method to determine the initial assignment of a stochastic local search algorithm through deep learning.Compared with the widely used random initialization method,the assignment generated by the method in this paper is closer to the solution of the problem.In this way,the search space is narrowed,and the number of flipping variables and running time of algorithm running will be reduced.In this paper,the satisfiable SAT problem dataset is considered as a data distribution,and deep learning is used to learn this distribution,so as to give a prediction of the initial assignment of the SAT problem.The initial assignment of stochastic local search is guided based on the results of the network.In this way,a pre-learning is performed on the distribution of SAT problems,and then stochastic local search is used on this basis to quickly solve problems.Second,this paper proposes a stochastic local search heuristic based on deep reinforcement learning.In stochastic local search algorithm,the process of finding a solution by flipping variables is the main step of the algorithm.Different heuristics determine different ways of search methods,and the goodness of the heuristics determines the final efficiency of different algorithms.In the process of training reinforcement learning model,the agent explores and utilizes a lot of data in the problem space.In this paper,the heuristic of stochastic local search is regarded as a reinforcement learning task,and the strategy of selecting flip variables is learned end-to-end through deep reinforcement learning.The problem examples obtained from the data set are used as the training environment,and the flip variables selected by the stochastic local search are used as the output of reinforcement learning model.In this way,the data learning ability of reinforcement learning is used to select smarter and more effective flip variables to improve the efficiency of the algorithm.In this paper,the performance and generalization ability of the two methods are tested on random 3-SAT problems and dominating set problems,and they are compared with the classical SAT solver Prob SAT.The experimental results show that from the perspective of SAT,methods in this paper can improve the efficiency of existing algorithms to a certain extent.And on the other hand,from the perspective of deep learning,methods in this paper have good generalization ability.