Configuration checking-based parallel model counting method

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. © 2020, Jilin University Press. All right reserved.