用于神经布尔可满足性问题求解器的新型消息传递网络

doi:10.11772/j.issn.1001-9081.2024091362

摘要/Abstract

摘要：

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

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

Abstract:

In order to optimize the structure of the Message Passing Neural Network （MPNN）， reduce the number of iterations in the solving process， and improve performance of end-to-end neural Boolean SATisfiability problem （SAT） solvers， a More and Deeper Message Passing Network （MDMPN） was proposed. In this network， to pass more messages， an overall message passing module was introduced， thereby realizing transmission of additional overall messages from literal nodes to clause nodes during each message passing iteration. At the same time， to pass deeper messages， a message jumping module was incorporated to realize transmission of messages from the 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 SAT solver QuerySAT and basic neural SAT solver NeuroSAT. Experimental results on the dataset of difficult random 3-SAT problems show that QuerySAT with MDMPN outperforms the standard QuerySAT with an accuracy improvement of 46.12 percentage points on difficult 3-SAT problem with 600 variables and iteration upper limit of 2¹²； NeuroSAT with MDMPN also outperforms the standard NeuroSAT with an accuracy improvement of 35.69 percentage points on difficult 3-SAT problem with 600 variables and iteration upper limit of 2¹².

Key words: Boolean SATisfiability problem (SAT), Message Passing Neural Network (MPNN), graph neural network, machine learning, artificial intelligence

中图分类号:

TP399

梁永濠, 李金龙. 用于神经布尔可满足性问题求解器的新型消息传递网络[J]. 计算机应用, 2025, 45(9): 2934-2940.

Yonghao LIANG, Jinlong LI. Novel message passing network for neural Boolean satisfiability problem solver[J]. Journal of Computer Applications, 2025, 45(9): 2934-2940.

图/表 11

参考文献 27

[1]	COOK S A. The complexity of theorem-proving procedures ［M］// Logic， automata， and computational complexity： the works of Stephen A. Cook. New York： ACM， 2023： 143-152.
[2]	VIZEL Y， WEISSENBACHER G， MALIK S. Boolean satisfiability solvers and their applications in model checking ［J］. Proceedings of the IEEE， 2015， 103（11）： 2021-2035.
[3]	KUEHLMANN A， PARUTHI V， KROHM F， et al. Robust Boolean reasoning for equivalence checking and functional property verification ［J］. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems， 2002， 21（12）： 1377-1394.
[4]	IVANČIĆ F， YANG Z， GANAI M K， et al. Efficient SAT-based bounded model checking for software verification ［J］. Theoretical Computer Science， 2008， 404（3）： 256-274.
[5]	PRASAD M R， BIERE A， GUPTA A. A survey of recent advances in SAT-based formal verification ［J］. International Journal on Software Tools for Technology Transfer， 2005， 7（2）： 156-173.
[6]	MIRONOV I， ZHANG L. Applications of SAT solvers to cryptanalysis of hash functions ［C］// Proceedings of the 2006 International Conference on Theory and Applications of Satisfiability Testing， LNCS 4121. Berlin： Springer， 2006： 102-115.
[7]	PLACHETTA R， VAN DER GRINTEN A. SAT-and-reduce for vertex cover： accelerating branch-and-reduce by sat solving ［C］// Proceedings of the 2021 Workshop on Algorithm Engineering and Experiments. Philadelphia， PA： SIAM， 2021： 169-180.
[8]	SKANSI S， ŠEKRST K， KARDUM M. A different approach for clique and household analysis in synthetic telecom data using propositional logic ［C］// Proceedings of the 43rd International Convention on Information， Communication and Electronic Technology. Piscataway： IEEE， 2020： 1286-1289.
[9]	VELEV M N. Exploiting hierarchy and structure to efficiently solve graph coloring as SAT ［C］// Proceedings of the 2007 IEEE/ACM International Conference on Computer-Aided Design. Piscataway： IEEE， 2007： 135-142.
[10]	郭莹，张长胜，张斌. 求解SAT问题的算法的研究进展［J］. 计算机科学， 2016， 43（3）：8-17.
	GUO Y， ZHANG C S， ZHANG B. Research advance of SAT solving algorithm ［J］. Computer Science， 2016， 43（3）：8-17.
[11]	谢志新，王晓峰，曹泽轩，等. 求解可满足性问题的信息传播算法研究综述［J］. 计算机应用研究， 2022， 39（7）：1933-1940.
	XIE Z X， WANG X F， CAO Z X， et.al. Overview of message propagation algorithm for satisfiability problems ［J］. Application Research of Computers， 2022， 39（7）：1933-1940.
[12]	GUO W， ZHEN H L， LI X， et al. Machine learning methods in solving the Boolean satisfiability problem ［J］. Machine Intelligence Research， 2023， 20（5）： 640-655.
[13]	AMIZADEH S， MATUSEVYCH S， WEIMER M. Learning to solve Circuit-SAT： an unsupervised differentiable approach ［EB/OL］. ［2024-03-12］..
[14]	ZHANG C， ZHANG Y， MAO J， et al. Towards better generalization for neural network-based sat solvers ［C］// Proceedings of the 2022 Pacific-Asia Conference on Knowledge Discovery and Data Mining， LNCS 13281. Cham： Springer， 2022： 199-210.
[15]	SELSAM D， LAMM M， BÜNZ B， et al. Learning a SAT solver from single-bit supervision ［EB/OL］. ［2024-04-15］..
[16]	OZOLINS E， FREIVALDS K， DRAGUNS A， et al. Goal-aware neural SAT solver［C］// Proceedings of the 2022 International Joint Conference on Neural Networks. Piscataway： IEEE， 2022： 1-8.
[17]	LI Z， SI X. NSNet： a general neural probabilistic framework for satisfiability problems ［C］// Proceedings of the 36th International Conference on Neural Information Processing Systems. Red Hook： Curran Associates Inc.， 2022： 25573-25585.
[18]	BIERE A， HEULE M， VAN MAAREN H， et al. Handbook of satisfiability ［M］. Amsterdam： IOS Press， 2009.
[19]	GILMER J， SCHOENHOLZ S S， RILEY P F， et al. Neural message passing for quantum chemistry ［C］// Proceedings of the 34th International Conference on Machine Learning. New York： JMLR.org， 2017： 1263-1272.
[20]	BATATIA I， KOVÁCS D P， SIMM G N C， et al. MACE： higher order equivariant message passing neural networks for fast and accurate force fields ［C］// Proceedings of the 36th International Conference on Neural Information Processing Systems. Red Hook： Curran Associates Inc.， 2022： 11423-11436.
[21]	TSEITIN G S. On the complexity of derivation in propositional calculus ［M］// SIEKMANN H， WRIGHTSON G. Automation of reasoning 2： classical papers on computational logic 1967—1970， SYMBOLIC. Berlin： Springer， 1983： 466-483.
[22]	BATTAGLIA P W， HAMRICK J B， BAPST V， et al. Relational inductive biases， deep learning， and graph networks ［EB/OL］. ［2024-09-23］..
[23]	SCARSELLI F， GORI M， TSOI A C， et al. The graph neural network mode l ［J］. IEEE Transactions on Neural Networks， 2008， 20（1）： 61-80.
[24]	龙峥嵘，李金龙，梁永濠. 基于SAT问题实例特性的端到端SAT求解模型［J］. 计算机应用研究， 2024， 41（11）： 3376-3381.
	LONG Z R， LI J L， LIANG Y H. End-to-end SAT assignment model based on instance related characteristics of SAT ［J］. Application Research of Computers， 2024， 41（11）： 3376-3381.
[25]	CRAWFORD J M， AUTON L D. Experimental results on the crossover point in random 3-SAT ［J］. Artificial Intelligence， 1996， 81（1/2）： 31-57.
[26]	LAURIA M， ELFFERS J， NORDSTRÖM J， et al. CNFGen： a generator of crafted benchmarks ［C］// Proceedings of the 2017 International Conference on Theory and Applications of Satisfiability Testing， LNCS 10491. Cham： Springer， 2017： 464-473.
[27]	CAMERON C， CHEN R， HARTFORD J， et al. Predicting propositional satisfiability via end-to-end learning ［C］// Proceedings of the 34th AAAI Conference on Artificial Intelligence. Palo Alto： AAAI Press， 2020： 3324-3331.

变量数	NeuroSAT的准确率/%		NeuroSAT-M的准确率/%		QuerySAT的准确率/%		QuerySAT-M的准确率/%		AEEV的准确率/%
变量数	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²
100	86.78	89.51	96.34	99.59	98.53	99.70	99.39	99.96	99.22	99.91
150	76.45	80.20	91.08	98.72	95.21	98.63	98.02	99.78	97.72	99.75
200	68.70	73.09	84.40	96.85	89.88	96.17	95.36	99.31	94.52	99.31
250	59.76	64.76	74.37	93.96	82.47	92.01	90.89	98.69	90.22	98.42
300	53.68	59.28	67.21	92.12	73.23	85.34	85.55	97.52	85.20	97.13
350	47.12	52.15	58.20	88.56	62.67	74.76	80.41	95.75	78.60	95.27
400	39.90	45.88	50.36	84.79	53.13	62.34	73.62	94.55	70.18	92.18
450	35.20	40.64	46.01	80.21	45.09	51.87	66.27	90.72	64.89	89.37
500	30.87	37.12	38.59	75.06	35.84	41.79	58.06	87.15	56.11	85.21
550	26.57	32.06	32.21	69.45	29.35	35.51	49.01	80.86	45.98	78.62
600	24.29	30.33	29.40	66.02	26.68	32.56	45.54	78.68	40.58	76.96

变量数	NeuroSAT的准确率/%		NeuroSAT-M的准确率/%		QuerySAT的准确率/%		QuerySAT-M的准确率/%		AEEV的准确率/%
变量数	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²	T=2⁹	T=2¹²
100	86.78	89.51	96.34	99.59	98.53	99.70	99.39	99.96	99.22	99.91
150	76.45	80.20	91.08	98.72	95.21	98.63	98.02	99.78	97.72	99.75
200	68.70	73.09	84.40	96.85	89.88	96.17	95.36	99.31	94.52	99.31
250	59.76	64.76	74.37	93.96	82.47	92.01	90.89	98.69	90.22	98.42
300	53.68	59.28	67.21	92.12	73.23	85.34	85.55	97.52	85.20	97.13
350	47.12	52.15	58.20	88.56	62.67	74.76	80.41	95.75	78.60	95.27
400	39.90	45.88	50.36	84.79	53.13	62.34	73.62	94.55	70.18	92.18
450	35.20	40.64	46.01	80.21	45.09	51.87	66.27	90.72	64.89	89.37
500	30.87	37.12	38.59	75.06	35.84	41.79	58.06	87.15	56.11	85.21
550	26.57	32.06	32.21	69.45	29.35	35.51	49.01	80.86	45.98	78.62
600	24.29	30.33	29.40	66.02	26.68	32.56	45.54	78.68	40.58	76.96

迭代次数上限	不同模块的准确率/%
迭代次数上限	QuerySAT	+O	+J	+O+J
2⁷	39.91	45.16	42.96	45.98
2⁸	47.35	55.76	56.68	61.13
2⁹	53.13	64.64	69.59	73.62
2¹⁰	56.91	72.13	79.51	82.90
2¹¹	59.96	77.57	85.27	89.44

迭代次数上限	不同模块的准确率/%
迭代次数上限	QuerySAT	+O	+J	+O+J
2⁷	39.91	45.16	42.96	45.98
2⁸	47.35	55.76	56.68	61.13
2⁹	53.13	64.64	69.59	73.62
2¹⁰	56.91	72.13	79.51	82.90
2¹¹	59.96	77.57	85.27	89.44

β	不同网络的准确率/%
β	NeuroSAT-M	QuerySAT-M
2³	40.39	21.42
2⁴	71.67	41.98
2⁵	89.59	78.65
2⁶	92.11	79.49
2⁷	91.23	78.28
2⁸	91.36	73.50