关键词: 布尔可满足性问题, 消息传递神经网络, 图神经网络, 机器学习, 人工智能

Abstract: In order to enhance the structure of the message passing network, reduce the number of iterations in the solving process, and consequently improve the solver’s performance, a novel More and Deeper Message Passing Network (MDMPN) for neural Boolean SATisfiability problem (SAT) solvers was proposed. To pass more messages, an overall-message passing module was introduced, which enabled the transmission of additional overall messages from literal nodes to clause nodes during each message passing iteration. Furthermore, to pass messages deeper, a message jumping module was incorporated, which facilitated the transmission of messages from literal nodes to their second-order neighbors. To assess the performance and generalizability of MDMPN, it was applied to the State-of-the-Art neural solver QuerySAT and basic neural solver NeuroSAT. Experimental results demonstrate that in solving difficult random 3-SAT problems, QuerySAT with MDMPN outperforms the standard QuerySAT, and improves the accuracy by 46.12 percentage points on difficult 3-SAT problems containing 600 variables. Similarly, NeuroSAT with MDMPN also outperforms the standard NeuroSAT, improving accuracy by 35.69 percentage points on difficult 3-SAT problems with 600 variables.

Key words: Boolean SATisfiability problem (SAT), message passing neural network, graph neural network, machine learning, artificial intelligence