软件学报

作者：贺甫霖,刘磊,吕帅,牛当当,王强

单位：贺甫霖，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001211,刘磊，吉林大学 计算机科学与技术学院, 吉林 长春 13001202,吕帅，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001203,牛当当，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 130012;西北农林科技大学 信息工程学院, 陕西 杨凌 71210004,王强，吉林大学 计算机科学与技术学院, 吉林 长春 130012;符号计算与知识工程教育部重点实验室(吉林大学), 吉林 长春 13001205

关键词：模型计数;局部搜索;格局检测

基金：国家自然科学基金（61300049，61763003）；吉林省自然科学基金（20180101053JC）

模型计数是指求出给定命题公式的模型数，是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用，很多现实问题都可以规约为模型计数进行求解.目前，常用的模型计数求解器主要有Cachet与sharpSAT，它们均采用完备方法且具有高效的求解能力，但其求解效率对模型数不敏感.有理由猜测：当给定问题的模型较少时，不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法，Cai等人提出了格局检测策略，并将其应用到局部搜索方法中，提出了SWcc算法，具有很高的求解效率.对SWcc算法进行扩充，分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法，给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果，以验证当给定合取范式的模型较少时，该迭代法与优化后的增量法的求解效率有所提升.

来源：2020年第2期

《软件学报》期刊编辑部

查看软件学报杂志2020年第2期