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

Configuration checking-based parallel model counting method

作　　者：李壮[1] 刘磊[1] 张桐搏 吕帅[1] LI Zhuang;LIU Lei;ZHANG Tong-bo;Lü Shuai(College of Computer Science and Technology,Jilin University,Changchun 130012,China)

机构地区：[1]吉林大学计算机科学与技术学院,长春130012

出　　处：《吉林大学学报（工学版）》2020年第4期1443-1448,共6页Journal of Jilin University:Engineering and Technology Edition

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

摘　　要：在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。Model counting has been widely used in solving classical satisfiability problems. In the case of benchmarks with few models,iterative Smoothed Weighting with configuration checking(SWcc)method and incremental SWcc optimized method are more applicable than other existed complete model counting methods. However,iterative SWcc method and incremental SWcc optimized method are both serial methods. There is no preprocessing strategy for the solution space in these methods,such as pruning or reduction. In order to mitigate this problem,we propose a new parallel model counting algorithm based on configuration checking in this paper. The algorithm concentrates on simplification and heuristics,the original solution space is decomposed into several subspaces and the original set of clauses is simplified.Then,these subspaces are processed in parallel. The experiment results show that our algorithm is more applicable than the original algorithm when solving benchmarks with fewer models and large-scale formulas.

关 键 词：自动推理 局部搜索 模型计数 格局检测 并行框架 

分 类 号：TP181[自动化与计算机技术—控制理论与控制工程]