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

摘要： 为优化端到端神经布尔可满足性问题(SAT)求解器的消息传递网络结构、减少求解过程中的迭代次数并提升求解器性能，提出一种新型的更多更深的消息传递网络（MDMPN）。该网络通过引入整体消息传递模块，在每次消息传递迭代中实现从文字节点到子句节点的额外的整体消息传递，以传递更多的消息。同时，通过引入消息跳跃模块，实现从文字节点到它的二阶邻居的消息传递，从而传递更深的消息。为了评估MDMPN的性能与泛化能力，将它应用于目前先进的神经SAT求解器QuerySAT和基础神经求解器NeuroSAT。实验结果表明，在困难随机3-SAT数据集上，应用MDMPN的QuerySAT求解性能优于标准的QuerySAT，在求解包含600个变量的困难3-SAT问题上准确率提高了46.12个百分点。应用MDMPN的NeuroSAT也优于标准的NeuroSAT，在求解包含600个变量的困难3-SAT问题上准确率提高了35.69个百分点。

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