基于消息传递关系网络的布尔可满足性预测
作者:
作者单位:

作者简介:

包冬庆(1996-),硕士生,CCF学生会员,主要研究领域为机器学习,形式化方法;
翟树茂(1998-),男,硕士生,CCF学生会员,主要研究领域为形式化方法,机器学习;
葛宁(1983-),女,副教授,博士生导师,CCF专业会员,主要研究领域为形式化方法,模型驱动,智能化软件工程;
张莉(1968-),女,教授,博士生导师,CCF杰出会员,主要研究领域为模型驱动,软件工程.

通讯作者:

张莉,E-mail:lily@buaa.edu.cn

中图分类号:

TP311

基金项目:

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


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

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    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.

    参考文献
    相似文献
    引证文献
引用本文

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

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号