Stochastic Local Search Algorithm Of SAT Based On Deep Learning And Probabilistic Reasoning

In stochastic local search algorithms of SAT problem,a randomly assigned strategy is usually employed in the initial assignment.Once there are too many locally optimal solutions around the initial value,the local search process will fall into the local minima and the search loop repeatedly,so the SAT's solving algorithm is highly dependent on the initial assignment.But it can learn from a lot of different instances by combination of deep learning technology and clustering method used to constrain the initial assignment of SAT search to make powerful abstraction of deep learning extract the structural features and implicit features optimizing the local search.In order to take advantage of the deep features for SAT and improve the efficiency of local search,this thesis represents the SAT formula with fixed-size graph embedding vectors by graph embedding of deep artificial neural networks.Different from the current SAT classifier based on deep learning,the model use the spatial pyramid pooling and residual neural network technology to explore profound semantic feature,and suggest adding auxiliary variable encoding to obtain the propensity information of each variable.Then we propose the concept of indirect weighted damage to consider the effect of argument flipping on clauses by the combination of knowledge learned in deep learning and statistical learning techniques in dynamic search process,and quantitative metrics is given.Finally we propose a local search algorithm based on deep learning and probabilistic reasoning algorithm,DL-PRsat.The DL-PRsat algorithm is compared with the local search algorithm of similar probabilistic reasoning,IBWsat,the current efficient local search algorithm,CSCCsat,and the CSCCsat* which uses the assignment-oriented initial value strategy proposed in this thesis.It shows that the initial assignment method mentioned in this thesis can improve the efficiency of local search algorithm in same certain extent.In addition,superior to IBWsat,the DL-PRsat is equivalent to the current excellent algorithm of the local search,and has advantages on difficult structured instances.