-
题名结合互补度的基于扩展规则#SAT问题求解方法
被引量:4
- 1
-
-
作者
欧阳丹彤
贾凤雨
刘思光
张立明
-
机构
吉林大学计算机科学与技术学院
符号计算与知识工程教育部重点实验室(吉林大学)
-
出处
《计算机研究与发展》
EI
CSCD
北大核心
2016年第7期1596-1604,共9页
-
基金
国家自然科学基金项目(61402196
61272208
+4 种基金
61133011
61003101
61170092)
中国博士后科学基金项目(2013M541302)
吉林省科技发展计划基金项目(20140520067JH)~~
-
文摘
#SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一,在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法 CER(counting models using extension rules)深入研究的基础上,提出一种结合互补度的#SAT问题求解方法.在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合,并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备.提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数.实验结果表明:与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足.
-
关键词
扩展规则
模型计数
cer方法
互补度
集合枚举树
-
Keywords
extension rule
model counting
cer (counting models using extension rules) algorithm
complementary degree
SE-Tree (set enumeration tree)
-
分类号
TP18
[自动化与计算机技术—控制理论与控制工程]
-