-
题名基于消息传递关系网络的布尔可满足性预测
被引量：1
- 1
-
-
作者
包冬庆
葛宁
翟树茂
张莉
-
机构
北京航空航天大学软件学院
北京航空航天大学计算机学院
软件开发环境国家重点实验室(北京航空航天大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2022年第8期2839-2850,共12页
-
基金
国家自然科学基金(61902011,61690202)
北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
-
文摘
布尔可满足性求解能够验证的问题规模通常受限,因此,如何高精度地预测其可满足性既是重要的研究问题,也是一项具有挑战性的工作.相关研究工作一般使用由文字节点和子句节点组成的图来表示布尔可满足性问题的结构,但是这种表征方法缺少了变量、子句之间的重要关系信息.在所提方法中,通过将原始布尔可满足性问题实例表征为多关系异构图的方式来表达变量和句子之间的关系,并设计使用消息传递关系网络模型来捕获实例的关系信息,提取了更多的结构特征.结果表明:该模型在预测精度、泛化能力和资源需求等方面均优于现有模型,对所选数据集的平均预测精度为81%.该模型在小规模问题(变量数为100)上训练,在大规模数据集上预测的平均预测精度达到了80.8%.同时,该模型对随机生成的非均匀随机问题的预测精度达到99%,这意味着它学习了预测可满足性的重要特征.此外,模型预测所花费的时间随着问题规模的增大也只是成线性增长.总结而言,基于关系消息传递网络提出了一个预测精度更高、泛化能力更好的布尔可满足性预测方法.
-
关键词
布尔可满足性问题
消息传递网络
结构特征
可满足性预测
多关系异构图
-
Keywords
Boolean satisfiability problem
message passing relation network
structure features
propositional satisfiability prediction
multirelational heterogeneous graph
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名共识协议的形式化验证研究现状与展望
- 2
-
-
作者
葛宁
贺俞凯
翟树茂
李晓洲
张莉
-
机构
北京航空航天大学软件学院
北京航空航天大学计算机学院
软件开发环境国家重点实验室(北京航空航天大学)
-
出处
《软件学报》
EI
CSCD
北大核心
2023年第11期4989-5007,共19页
-
基金
国家重点研发计划(2018YFB1402700)
国家自然科学基金(61902011)
北京航空航天大学软件开发环境国家重点实验室开放课题(SKLSDE-2021ZX-01)。
-
文摘
分布式系统在计算环境中发挥重要的作用,其中的共识协议算法用于保证节点间行为的一致性.共识协议的设计错误可能导致系统运行故障,严重时可能对人员和环境造成灾难性的后果,因此保证共识协议设计的正确性非常重要.形式化验证能够严格证明设计模型中目标性质的正确性,适合用于验证共识协议.然而,随着分布式系统的规模增大,问题复杂度提升,使得分布式共识协议的形式化验证更为困难.采用什么方法对共识协议的设计进行形式化验证、如何提升验证规模,是共识协议形式化验证的重要研究问题.对目前采用形式化方法验证共识协议的研究工作进行调研,总结其中提出的重要建模方法和关键验证技术,并展望该领域未来有潜力的研究方向.
-
关键词
共识协议
形式化验证
限界模型检测
定理证明
布尔表达式可满足性理论
可满足性模理论
-
Keywords
consensus protocol
formal verification
bounded model checking
theorem proving
Boolean satisfiability problem(SAT)
satisfiability module theory(SMT)
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
