软件学报

作者：包冬庆，葛宁，翟树茂，张莉

单位：包冬庆，北京航空航天大学 软件学院, 北京 10019111,葛宁，北京航空航天大学 软件学院, 北京 100191;软件开发环境国家重点实验室(北京航空航天大学), 北京 10019102,翟树茂，北京航空航天大学 软件学院, 北京 10019103,张莉，北京航空航天大学 软件学院, 北京 100191;北京航空航天大学 计算机学院, 北京 100191;软件开发环境国家重点实验室(北京航空航天大学), 北京 10019104

关键词：布尔可满足性问题;消息传递网络;结构特征;可满足性预测;多关系异构图

基金：国家自然科学基金(61902011,61690202);北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)

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

来源：2022年第8期

《软件学报》期刊编辑部

查看软件学报杂志2022年第8期