一种基于扩展规则的#SAT求解系统

• 作者: 孙吉贵 林海 殷明浩
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 扩展规则 模型计数 知识编译 加权模型计数
• 年，卷（期）: 2009,（7）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 1714-1725
• 页数: 12页
• 分类号: TP18
• 字数: 9636字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2009.03320

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙吉贵	吉林大学计算机科学与技术学院	134	2984	21.0	52.0
5	殷明浩	吉林大学计算机科学与技术学院	35	304	10.0	16.0
8	林海	吉林大学计算机科学与技术学院	31	100	6.0	8.0