摘要
布尔可满足性求解能够验证的问题规模通常受限,因此,如何高精度地预测其可满足性既是重要的研究问题,也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构,但是这种表征方法缺少了变量、子句之间的重要关系信息.在所提方法中,通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系,并设计使用消息传递关系网络模型来捕获实例的关系信息,提取了更多的结构特征.结果表明:该模型在预测精度、泛化能力和资源需求等方面均优于现有模型,对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练,在大规模数据集上预测的平均预测精度达到了80.8%.同时,该模型对随机生成的非均匀随机问题的预测精度达到99%,这意味着它学习了预测可满足性的重要特征.此外,模型预测所花费的时间随着问题规模的增大也只是成线性增长.总结而言,基于关系消息传递网络提出了一个预测精度更高、泛化能力更好的布尔可满足性预测方法.
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.
作者
包冬庆
葛宁
翟树茂
张莉
BAO Dong-Qing;GE Ning;ZHAI Shu-Mao;ZHANG Li(College of Software,Beihang University,Beijing 100191,China;School of Computer Science and Engineering,Beihang University,Beijing 100191,China;State Key Laboratory of Software Development Environment(Beihang University),Beijing 100191,China)
出处
《软件学报》
EI
CSCD
北大核心
2022年第8期2839-2850,共12页
Journal of Software
基金
国家自然科学基金(61902011,61690202)
北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
关键词
布尔可满足性问题
消息传递网络
结构特征
可满足性预测
多关系异构图
Boolean satisfiability problem
message passing relation network
structure features
propositional satisfiability prediction
multirelational heterogeneous graph