| 间接使用扩展规则求解#SAT问题 |
| |
| 引用本文： | 许有军,欧阳丹彤,叶育鑫,何加亮. 间接使用扩展规则求解#SAT问题[J]. 吉林大学学报(工学版), 2011, 0(4): 1047-1053 |
| |
| 作者姓名： | 许有军 欧阳丹彤 叶育鑫 何加亮 |
| |
| 作者单位： | 吉林大学计算机科学与技术学院;吉林大学符号计算与知识工程教育部重点实验室; |
| |
| 基金项目： | 国家自然科学基金重大项目(60496320,60496321),国家自然科学基金项目(60973089,60773097,60873148); 吉林省科技发展计划项目(20080107); 欧盟合作项目(155776-EM-1-2009-1-IT-ERAMUN-DUS-ECW-L12) |
| |
| 摘 要： | 针对求解#SAT问题时算法时间会随着子句集的规模迅速增加的问题,提出一种间接应用扩展规则的MCEHST算法。该算法首先求出子句集的所有极小碰集,然后应用扩展规则计算这些极小碰集所能扩展出的极大项的数量,即模型数。实验结果表明:MCEHST算法运行时间随子句集规模增加的速度要比CDP和CER算法慢;当子句的长度较短、子句数较多时,MCEHST算法的时间效率较高。
|
| 关 键 词： | 人工智能 自动推理 扩展规则 碰集 CDP算法 CER算法 |
Solving #SAT with extension rule indirectly |
| |
| XU You-jun,,OUYANG Dan-tong,YE Yu-xin,HE Jia-liang. Solving #SAT with extension rule indirectly[J]. Journal of Jilin University:Eng and Technol Ed, 2011, 0(4): 1047-1053 |
| |
| Authors: | XU You-jun OUYANG Dan-tong YE Yu-xin HE Jia-liang |
| |
| Affiliation: | XU You-jun1,2,OUYANG Dan-tong1,YE Yu-xin1,HE Jia-liang1,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,China) |
| |
| 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 prop... |
| |
| Keywords: | artificial intelligence automated reasoning extension rule hitting set CDP algorithm CER algo rithm |
| 本文献已被 CNKI 等数据库收录！ |
|
