A Heuristic SAT Problems Solving Method based on LSTM Network

Boolean Satisfiability Problem(SAT) is a well known determination Problem. S.A.Cook proved in 1971 that SAT Problem is the first NP-Complete (NPC) Problem in the world, namely, any non-deterministic Polynomial (NP) Problem can be specified with the SAT Problem for solving in Polynomial time. Therefore, Boolean satisfiability problem (SAT) can be extended to many practical applications, such as integrated circuit design optimization, biological genes, artificial intelligence, Internet, etc. And there are a lot of NP problems in cryptography. Therefore, the study of SAT Problem is of great significance to cryptography. In this paper, we design a heuristic SAT solving algorithm based on LSTM (Long Short-Term Memory) recurrent neural networks. First of all, based on LSTM, we train the model as an end-to-end SAT Solver, which can output 0 or 1 to represent the satisfiability of each SAT problem. Then we extract the highdimensional output of the LSTM network and carry out k-means clustering analysis. Finally, we assign the obtained results as the initial value of the variables of the SAT problem, and inspire two types of classical algorithms (complete algorithm and incomplete algorithm) to solve the SAT problem respectively, so as to accelerate the solving process. In the experiment, we demonstrated the test results of SAT problems with different sizes, and The results show that the LSTM-WalkSAT and LSTM-DPLL based heuristic SAT solving methods can significantly improve the solving efficiency of the original complete or incomplete SAT solving algorithms.