欧阳丹彤　贾凤雨　刘思光　张立明

(吉林大学计算机科学与技术学院　长春　130012) (符号计算与知识工程教育部重点实验室(吉林大学)　长春　130012)



结合互补度的基于扩展规则#SAT问题求解方法

欧阳丹彤贾凤雨刘思光张立明

(吉林大学计算机科学与技术学院长春130012) (符号计算与知识工程教育部重点实验室(吉林大学)长春130012)

(ouyd@jlu.edu.cn)

摘要#SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一，在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法CER(counting models using extension rules)深入研究的基础上，提出一种结合互补度的#SAT问题求解方法.在计算给定子句集的模型个数时，利用SE-Tree(set enumeration tree)形式化地表达计算过程，逐步生成需要计算的子句集合，并在SE-Tree中添加终止结点，避免大部分含互补文字子句集合的生成，且不会因剪枝而导致求解不完备.提出互补度的概念，在扩展SE-Tree结点时按照互补度由大到小的顺序扩展，较早地生成含互补文字且长度较小的子句集合，有效减少枚举树生成的结点个数，进而减少对子句集合判断是否含互补文字的计算次数.实验结果表明：与CER方法相比该方法效率较好，且进一步改进了CER方法在互补因子较低时求解效率低下的不足.

关键词扩展规则；模型计数；CER方法；互补度；集合枚举树

命题可满足问题(propositional satisfiability problem, SAT)是人工智能领域中关键研究问题，有着相当广泛的应用，如在智能规划领域将规划问题编译成SAT问题进行求解[1]，同样地其还被应用于求解基于模型的诊断问题……