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

作     者：李壮 刘磊 张桐搏 吕帅 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优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。