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

布尔可满足性求解能够验证的问题规模通常受限, 因此, 如何高精度地预测布尔可满足性问题的可满足性是一个重要研究问题, 也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构, 但是这种表征方法缺少了变量、子句之间的重要关系信息.在我们的方法中, 通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系, 并设计使用消息传递关系网络模型来捕获实例的关系信息, 提取了更多的结构特征.结果表明, 该模型在预测精度、泛化能力和资源需求等方面均优于现有模型, 对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练, 在大规模数据集上预测的平均预测精度达到了80.8%.同时, 该模型对随机生成的非均匀随机问题的预测精度达到99%, 这意味着它学习了预测可满足性的重要特征.此外, 模型预测所花费的时间随着问题规模的增大也只是呈线性增长. 总结而言, 本文基于关系消息传递网络提出了一个预测精度更高, 泛化能力更好的布尔可满足性预测方法.

Predicting Propositional Satisfiability via Message Passing Relation Network

The scale of problems that can be verified by boolean satisfiability 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. We encode raw SAT instances to multi-relational heterogeneous graphs and use a message passing relation (MPR) network model to capture more structure features of a SAT instance. We showed that the MPR network model could outperform previous work in terms of prediction accuracy, generalization ability, and resource requirement. We achieved an average prediction accuracy of 81% on all datasets. The model trained on small-scale problems (the number of variables is 100) achieved 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, this paper proposes a method with higher prediction accuracy and better generalization ability based on a relational messaging network to predict propositional satisfiability.