咨询与建议

看过本文的还看了

相关文献

该作者的其他文献

文献详情 >基于格局检测的并行模型计数方法 收藏

基于格局检测的并行模型计数方法

Configuration checking-based parallel model counting method

作     者:李壮 刘磊 张桐搏 吕帅 LI Zhuang;LIU Lei;ZHANG Tong-bo;Lü Shuai

作者机构:吉林大学计算机科学与技术学院长春130012 

出 版 物:《吉林大学学报(工学版)》 (Journal of Jilin University:Engineering and Technology Edition)

年 卷 期:2020年第50卷第4期

页      面:1443-1448页

核心收录:

学科分类:12[管理学] 1201[管理学-管理科学与工程(可授管理学、工学学位)] 081104[工学-模式识别与智能系统] 08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术(可授工学、理学学位)] 

基  金:国家重点研发计划项目(2017YFB1003103) 国家自然科学基金项目(61300049,61763003) 吉林省自然科学基金项目(20180101053JC,20190201193JC) 吉林大学研究生创新基金项目(101832018C025) 

主  题:自动推理 局部搜索 模型计数 格局检测 并行框架 

摘      要:在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。

读者评论 与其他读者分享你的观点

用户名:未登录
我的评分