间接使用扩展规则求解#SAT问题

吉林大学学报(工学版) ›› 2011, Vol. 41 ›› Issue (4): 1047-1053.

间接使用扩展规则求解#SAT问题

许有军^1,2,欧阳丹彤^1,2,叶育鑫^1,2,何加亮^1,2

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

收稿日期:2010-05-12 出版日期:2011-07-01 发布日期:2011-07-01
通讯作者: 欧阳丹彤（1968-），女，教授，博士生导师.研究方向:基于模型的诊断、自动推理等. E-mail:ouyangdantong@163.com
作者简介:许有军（1977-)|男|博士研究生.研究方向:自动推理. E-mail:xuyj_jlu@yeah.net
基金资助:
国家自然科学基金重大项目(60496320, 60496321);国家自然科学基金项目(60973089,60773097, 60873148)；吉林省科技发展计划项目(20080107)；欧盟合作项目(155776-EM-1-2009-1-IT-ERAMUN-DUS- ECW-L12).

Solving #SAT with extension rule indirectly

XU You-jun^1,2,OUYANG Dan-tong^1,2,YE Yu-xin^1,2,HE Jia-liang^1,2

1.College of Computer Science and Technology, Jilin University, Changchun 130012, China|2.Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University, Changchun 130012, China

Received:2010-05-12 Online:2011-07-01 Published:2011-07-01

摘要/Abstract

摘要：

针对求解#SAT问题时算法时间会随着子句集的规模迅速增加的问题，提出一种间接应用扩展规则的MCEHST算法。该算法首先求出子句集的所有极小碰集，然后应用扩展规则计算这些极小碰集所能扩展出的极大项的数量，即模型数。实验结果表明：MCEHST算法运行时间随子句集规模增加的速度要比CDP和CER算法慢；当子句的长度较短、子句数较多时，MCEHST算法的时间效率较高。

关键词: 人工智能, 自动推理, 扩展规则, 碰集, CDP算法, CER算法

Abstract:

Satisfiability (#SAT) is an important problem in artificial intelligence. May algorithms for solving #SAT problem are only appropriate for small clause number. The runtime increases rapidly with the enhancement of clause sets' scale. We propose a new algorithm, named MCEHST, using extension rule indirectly. There two steps in this method. The first step calculates all minimal hitting sets of a clause set. The second step counts models with these hitting sets using extension rule. Experiment results show that the proposed MCEHST is more efficient than CDP and CER under large clause number and short clause length. Using MCEHST the increase in runtime is slower than CDP and CER.

Key words: artificial intelligence, automated reasoning, extension rule, hitting set, CDP algorithm, CER algorithm

中图分类号:

TP181

许有军^1,2,欧阳丹彤^1,2,叶育鑫^1,2,何加亮^1,2. 间接使用扩展规则求解#SAT问题[J]. 吉林大学学报(工学版), 2011, 41(4): 1047-1053.

XU You-jun,OUYANG Dan-tong,YE Yu-xin,HE Jia-liang. Solving #SAT with extension rule indirectly[J]. 吉林大学学报(工学版), 2011, 41(4): 1047-1053.

参考文献

相关文章 15

[1]	董飒, 刘大有, 欧阳若川, 朱允刚, 李丽娜. 引入二阶马尔可夫假设的逻辑回归异质性网络分类方法[J]. 吉林大学学报(工学版), 2018, 48(5): 1571-1577.
[2]	顾海军, 田雅倩, 崔莹. 基于行为语言的智能交互代理[J]. 吉林大学学报(工学版), 2018, 48(5): 1578-1585.
[3]	王旭, 欧阳继红, 陈桂芬. 基于垂直维序列动态时间规整方法的图相似度度量[J]. 吉林大学学报(工学版), 2018, 48(4): 1199-1205.
[4]	张浩, 占萌苹, 郭刘香, 李誌, 刘元宁, 张春鹤, 常浩武, 王志强. 基于高通量数据的人体外源性植物miRNA跨界调控建模[J]. 吉林大学学报(工学版), 2018, 48(4): 1206-1213.
[5]	黄岚, 纪林影, 姚刚, 翟睿峰, 白天. 面向误诊提示的疾病-症状语义网构建[J]. 吉林大学学报(工学版), 2018, 48(3): 859-865.
[6]	李雄飞, 冯婷婷, 骆实, 张小利. 基于递归神经网络的自动作曲算法[J]. 吉林大学学报(工学版), 2018, 48(3): 866-873.
[7]	刘杰, 张平, 高万夫. 基于条件相关的特征选择方法[J]. 吉林大学学报(工学版), 2018, 48(3): 874-881.
[8]	王旭, 欧阳继红, 陈桂芬. 基于多重序列所有公共子序列的启发式算法度量多图的相似度[J]. 吉林大学学报(工学版), 2018, 48(2): 526-532.
[9]	杨欣, 夏斯军, 刘冬雪, 费树岷, 胡银记. 跟踪-学习-检测框架下改进加速梯度的目标跟踪[J]. 吉林大学学报(工学版), 2018, 48(2): 533-538.
[10]	刘雪娟, 袁家斌, 许娟, 段博佳. 量子k-means算法[J]. 吉林大学学报(工学版), 2018, 48(2): 539-544.
[11]	曲慧雁, 赵伟, 秦爱红. 基于优化算子的快速碰撞检测算法[J]. 吉林大学学报(工学版), 2017, 47(5): 1598-1603.
[12]	李嘉菲, 孙小玉. 基于谱分解的不确定数据聚类方法[J]. 吉林大学学报(工学版), 2017, 47(5): 1604-1611.
[13]	邵克勇, 陈丰, 王婷婷, 王季驰, 周立朋. 无平衡点分数阶混沌系统全状态自适应控制[J]. 吉林大学学报(工学版), 2017, 47(4): 1225-1230.
[14]	王生生, 王创峰, 谷方明. OPRA方向关系网络的时空推理[J]. 吉林大学学报(工学版), 2017, 47(4): 1238-1243.
[15]	马淼, 李贻斌. 基于多级图像序列和卷积神经网络的人体行为识别[J]. 吉林大学学报(工学版), 2017, 47(4): 1244-1252.

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed