基于消息传递关系网络的布尔可满足性预测

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.