论文部分内容阅读
#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT求解系统:JLU-ERWMC.实验结果表明,JLU-ERWMC在有些问题中优于目前最为高效的#SAT问题求解系统.
#SAT problem is an extension of SAT problem, which requires calculating the number of models for a given set of propositional formulas. By solving the problem along the direction of the boil down and using the principle of exclusion to solve the problem of spatial complexity, This paper proposes a framework for solving the problem of model counting and weighted model counting based on extended rules, which can be regarded as a complementary method for solving all current model counting problems. The completeness and validity of the proposed method are proved. The regular #SAT solution system: JLU-ERWMC. The experimental results show that JLU-ERWMC outperforms the most efficient #SAT problem solving system in some problems.