Abstract

Machine Learning for SAT (ML4SAT) offers a data-driven alternative to traditional solvers. However, existing flat-vector paradigms face scalability bottlenecks, feature redundancy, and struggle to exploit the intrinsic logical structures of clauses. To address these deficiencies, a novel encoding and enhancement paradigm is proposed, comprising: (1) a lightweight Prime-Product Clause Encoding (PPCE) scheme leveraging unique prime factorization for mathematically lossless dimensionality compression; (2) a Structure-Aware Enhancement (SAE) module incorporating a localized subnetwork (ClauseNet) to better capture intraclause logic; and (3) a controlled benchmark evaluating four canonical models—Logistic Regression, Support Vector Machine, Multi-Layer Perceptron, and Transformer—under unified variables. Empirical results on two large-scale CNF datasets (183k and 480k samples) reveal high-dimensional semi-sparsity (S ranging from 73.81% to 75.20%). PPCE reduces feature dimensionality by 75%, while the SAE module can improve accuracy across models without inference overhead. These findings validate specialized encoding and structural modules in ML4SAT, providing practical, data-driven selection guidelines for exploring accuracy-efficiency trade-offs in industrial formal verification.

References

• A. Biere, M. Heule, H. van Maaren, and T. Walsh. Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, 2021.
• H. K. B¨uning and T. Lettmann. Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge, England, 1999.
• W. J. Chang, M. Y. Guo, and J. W. Luo. Predicting the satisfiability of Boolean formulas by incorporating gated recurrent unit (GRU) in the Transformer framework. PeerJ Computer Science, 10:e2169, October 2024.
• Y. J. Chang, M. S. M. Mohd Kasihmuddin, W. N. A. Ruzai, Y. Guo, and J. Chen. Weighted C-type random 2 satisfiability in discrete Hopfield neural network. Engineering Applications of Artificial Intelligence, 160:111760, April 2025.
• Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC), pages 151–158, New York, NY, USA, 1971. ACM.
• C. Cortes and V. Vapnik. Support-vector networks. Machine Learning, 20(3):273–299, September 1995.
• D. R. Cox. The regression analysis of binary sequences. Journal of the Royal Statistical Society: Series B (Methodological), 20(2):215–232, June 1958.
• R. Gor´e. Tableau methods for modal and temporal logics. Tech. Rep. TR-ARP-15-95, Australian National University, November 1995.
• M. Gori, G. Monfardini, and F. Scarselli. A new model for learning in graph domains. In Proceedings of the 2005 IEEE International Joint Conference on Neural Networks (IJCNN), pages 729–734. IEEE, 2005.
• J. J. Hopfield. Neural networks and physical systems with emergent collective computational abilities. Proceedings of the National Academy of Sciences, 79(8):2554–2558, April 1982.
• J. H˚ula, D. Mojˇz´ıˇsek, and M. Janota. Understanding GNNs for Boolean satisfiability through approximation algorithms. In Proceedings of the 33rd ACM International Conference on Information and Knowledge Management (CIKM), pages 953–961, New York, NY, USA, 2024. ACM.
• D. Jia, X. Duan, and M. K. Khan. Binary artificial bee colony optimization using bitwise operation. Computers & Industrial Engineering, 76:360–365, October 2014.
• D. S. Johnson. Approximation algorithms for combinatorial problems. Journal of Computer and System Sciences, 9(3):256–278, September 1974.
• Y. J. Li, T. Zhang, and H. H. Hu. Deep kernel mapping support vector machines based on multi-layer perceptron. Journal of Beijing University of Technology, 42(11):1652–1661, November 2016.
• Y. H. Liang and J. L. Li. Novel message passing network for neural Boolean satisfiability problem solver. Journal of Computer Applications, 45(9):2934–2940, September 2025.
• J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23–41, January 1965.
• D. E. Rumelhart, G. E. Hinton, and R. J. Williams. Learning representations by back-propagating errors. Nature, 323(6088):533–536, October 1986.
• K. Schneider. Verification of Reactive Systems: Formal Methods and Algorithms. Springer, Berlin, Germany, 2004.
• D. Selsam and N. Bjørner. Guiding high-performance SAT solvers with unsat-core predictions. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), pages 336–353, Cham, Switzerland, 2019. Springer.
• D. Selsam, M. Lamm, B. B¨unz, P. Liang, D. L. Dill, and L. de Moura. Learning a SAT solver from single-bit supervision. In Proceedings of the 7th International Conference on Learning Representations (ICLR), 2019. Published online via OpenReview, no numerical pages assigned.
• E. Shoham, H. Cohen, K. Wattad, et al. Concept learning for algorithmic reasoning: Insights from SAT-solving GNNs. Information Sciences, 726:122754, June 2026.
• Y. W. Sun, F. R. Ye, X. Y. Zhang, et al. AutoSAT: Automatically optimize SAT solvers via large language models. arXiv preprint arXiv:2402.10705, February 2024.
• A. Vaswani, N. Shazeer, N. Parmar, J. Uszkoreit, L. Jones, A. N. Gomez, Ł. Kaiser, and I. Polosukhin. Attention is all you need. In Proceedings of the 31st International Conference on Advances in Neural Information Processing Systems (NIPS 2017), pages 5998–6008, Red Hook, NY, USA, 2017. Curran Associates, Inc.
• C. X. Yu, R. J. Liang, C. T. Ho, et al. Autonomous code evolution meets NP-completeness. arXiv preprint arXiv:2509.07367, September 2025.