论文部分内容阅读
#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数,通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT求解系统:JLU-ERWMC,实验结果表明,JLU-ERWMC在有些问题中优于目前最为高效的#SAT问题求解系统.