Research On The Satisfaction Determination Of SAT Problem And Its All Solutions

The satisfiability problem(SAT)plays an important role in mathematics and computer science,and is can be regarded as the cornerstone of application in the fields of industrial automation.the machine learning approach aiming at SAT is still young now,that means,the existing method didn't try to solve the large and difficult problems.this thesis designs effective machine learning methods for large-scale and hard satisfiability problems.While the All Solution satisfiability problem(ALLSAT)is more widely used in industry practice and has higher demand for technology.Since the computational complexity of the all solution of SAT is higher than that of the general SAT problem,there is a lack of relevant research so far,and the solving ability of the corresponding solver is general.Therefore,Basing on all these above,we make a comprehensive study on the All Solution satisfiability problem and design an effective method for solving ALLSAT problems.Considering that the SAT can be regarded as binary classification problems,the determination of the SAT problem as supervised binary classification problems,we propose two methods to classify SAT problem.The first is a solution method based on traditional machine learning.This method calculates the features of SAT,with a total number of141 features,and then puts them into the selected traditional machine learning model for training.the principle of model selection is based on the solving characteristics of SAT problems and the training efficiency and accuracy of the model.The second bases on deep learning.Firstly,the satisfability problem is encoded into a numerical matrix.In this thesis,three matrix transformation methods are introduced,and an optimal transformation scheme is found through analysis.The experimental results show that the proposed method based on LightGBM model can predict the satisfiability problem quickly and accurately,and achieves a accuracy of 0.966 on the agile17 data set.The accuracy of CNN based model can reach an accuracy above 0.9 in a single category of datasets.The machine learning-based SAT solving method can to solve large-scale and complex SAT problems to some extent.Aiming at the all solution satisfiability problem,we introduce a divide-and-conquerbased algorithm,two segmentation strategies are proposed,including Jaccard similarity segmentation and variable complementation segmentation.The experimental result shows that the method proposed in this paper,has a better performance than the state-ofthe-art algorithms,with regarding to the number of instances solved and the total number of solutions found for SAT 2014 competition benchmark.