Predicting Propositional Satisfiability via Message Passing Relation Network
Author:
Affiliation:

Clc Number:

TP311

  • Article
  • | |
  • Metrics
  • |
  • Reference [29]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    The scale of problems that can be verified by Boolean satisfiability (SAT) solving is usually limited. Therefore, how to predict the satisfiability of SAT problems with high accuracy is an important research problem and also a challenging task. Previous works used graphs consisting of literal nodes and clause nodes to represent the structure of SAT problems. The important relation information between variables and clauses is missing. Raw SAT instances are encoded to multi-relational heterogeneous graphs and a message passing relation (MPR) network model is used to capture more structure features of an SAT instance. It is showed that the MPR network model could outperform previous work in terms of prediction accuracy, generalization ability, and resource requirement. An average prediction accuracy of 81% is achieved on all datasets. The model trained on small-scale problems (the number of variables is 100) achieves an average prediction accuracy of 80.8% on larger-scale datasets. Prominently, this model gets 99% prediction accuracy on the randomly generated non-uniform random SAT problems, which means it has learned important features to predict satisfiability. Moreover, the running time for prediction increases linearly with the size of the problem. In conclusion, the proposed method is of higher prediction accuracy and better generalization ability based on a relational messaging network to predict propositional satisfiability.

    Reference
    [1] Mitchell D, Selman B, Levesque H.Hard and easy distributions of SAT problems.AAAI, 1992, 92:459-465.
    [2] Cheeseman PC, Kanefsky B, Taylor WM.Where the really hard problems are.IJCAI, 1991, 91:331-337.
    [3] Mu Z, Hoos HH.On the empirical time complexity of random 3-SAT at the phase transition.In:Proc.of the 24th Int'l Joint Conf.on Artificial Intelligence.2015.
    [4] Sandholm TW.A second order parameter for 3SAT.In:Proc.of the AAAI-96.1996.259-265.
    [5] Xu L, Hoos H, Leyton-Brown K.Predicting satisfiability at the phase transition.In:Proc.of the 26th AAAI Conf.on Artificial Intelligence, 2012.584-590.
    [6] Nudelman E, Leyton-Brown K, Hoos HH, et al.Understanding random SAT:Beyond the clauses-to-variables ratio.In:Proc.of the Int'l Conf.on Principles and Practice of Constraint Programming.Berlin, Heidelberg:Springer, 2004.438-452.
    [7] Xu L, Hutter F, Hoos H, et al.Features for SAT.Technology Report, Vancouver:University of British Columbia, 2012.
    [8] Liang JH, Oh C, Mathew M, et al.Machine learning-based restart policy for CDCL SAT solvers.In:Proc.of the Int'l Conf.on Theory and Applications of Satisfiability Testing.Cham:Springer, 2018.94-110.
    [9] Li Z, Chen Q, Koltun V.Combinatorial optimization with graph convolutional networks and guided tree search.In:Proc.of the Advances in Neural Information Processing Systems.2018.539-548.
    [10] Selsam D, Bjørner N.Guiding high-performance SAT solvers with unsat-core predictions.In:Proc.of the Int'l Conf.on Theory and Applications of Satisfiability Testing.Cham:Springer, 2019.336-353.
    [11] Loreggia A, Malitsky Y, Samulowitz H, et al.Deep learning for algorithm portfolios.In:Proc.of the 30th AAAI Conf.on Artificial Intelligence.2016.
    [12] Bünz B, Lamm M.Graph neural networks and Boolean satisfiability.arXiv:1702.03592, 2017.
    [13] Selsam D, Lamm M, Bünz B, et al.Learning a SAT solver from single-bit supervision.In:Proc.of the ICLR (Poster).2019.
    [14] Cameron C, Chen R, Hartford J, et al.Predicting propositional satisfiability via end-to-end learning.Proc.of the AAAI Conf.on Artificial Intelligence, 2020, 34(4):3324-3331.
    [15] Gilmer J, Schoenholz SS, Riley PF, et al.Neural message passing for quantum chemistry.In:Proc.of the Int'l Conf.on Machine Learning.PMLR, 2017.1263-1272.
    [16] Schlichtkrull M, Kipf TN, Bloem P, et al.Modeling relational data with graph convolutional networks.In:Proc.of the European Semantic Web Conf.Cham:Springer, 2018.593-607.
    [17] Duvenaud D, Maclaurin D, Aguilera-Iparraguirre J, et al.Convolutional networks on graphs for learning molecular fingerprints.In:Proc.of the NIPS.2015.2224-2232.
    [18] Hochreiter S, Schmidhuber J.Long short-term memory.Neural Computation, 1997, 9(8):1735-1780.
    [19] Elman JL.Finding structure in time.Cognitive Science, 1990, 14(2):179-211.
    [20] Li Y, Tarlow D, Brockschmidt M, et al.Gated graph sequence neural networks.arXiv:1511.05493, 2015.
    [21] Crawford JM, Auton LD.Experimental results on the crossover point in random 3-SAT.Artificial Intelligence, 1996, 81(1-2):31-57.
    [22] Lauria M, Elffers J, Nordström J, et al.CNFgen:A generator of crafted benchmarks.In:Proc.of the Int'l Conf.on Theory and Applications of Satisfiability Testing.Cham:Springer, 2017.464-473.
    [23] Glorot X, Bordes A, Bengio Y.Deep sparse rectifier neural networks.In:Proc.of the 14th Int'l Conf.on Artificial Intelligence and Statistics.2011.315-323.
    [24] Kingma DP, Ba J.Adam:A method for stochastic optimization.arXiv:1412.6980, 2014.
    [25] Van der Maaten L, Hinton G.Visu-Alizing data using t-SNE.Journal of Machine Learning Research, 2008.2579-2605.
    [26] Zhang H, Stickel M.Implementing the davis-putnam method.Journal of Automated Reasoning, 2000, 24(1):277-296.
    [27] Simon L, Audemard G.Predicting learnt clauses quality in modern sat solver.In:Proc.of the 21st Int'l Joint Conf.on Artificial Intelligence (IJCAI 2009).2009.
    [28] Braunstein A, Mézard M, Zecchina R.Survey propagation:An algorithm for satisfiability.Random Structures&Algorithms, 2005, 27(2):201-226.
    [29] Hartford J, Graham D, Leyton-Brown K, et al.Deep models of interactions across sets.In:Proc.of the Int'l Conf.on Machine Learning.PMLR, 2018.1909-1918.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

包冬庆,葛宁,翟树茂,张莉.基于消息传递关系网络的布尔可满足性预测.软件学报,2022,33(8):2839-2850

Copy
Share
Article Metrics
  • Abstract:994
  • PDF: 3634
  • HTML: 3027
  • Cited by: 0
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: August 06,2022
You are the first2036712Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063