版权所有:内蒙古大学图书馆 技术提供:维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
作者机构:吉林大学计算机科学与技术学院长春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优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。