摘要
针对求解#SAT问题时算法时间会随着子句集的规模迅速增加的问题,提出一种间接应用扩展规则的MCEHST算法。该算法首先求出子句集的所有极小碰集,然后应用扩展规则计算这些极小碰集所能扩展出的极大项的数量,即模型数。实验结果表明:MCEHST算法运行时间随子句集规模增加的速度要比CDP和CER算法慢;当子句的长度较短、子句数较多时,MCEHST算法的时间效率较高。
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.
出处
《吉林大学学报（工学版）》
EI
CAS
CSCD
北大核心
2011年第4期1047-1053,共7页
Journal of Jilin University:Engineering and Technology Edition
基金
国家自然科学基金重大项目(60496320
60496321)
国家自然科学基金项目(60973089
60773097
60873148)
吉林省科技发展计划项目(20080107)
欧盟合作项目(155776-EM-1-2009-1-IT-ERAMUN-DUS-ECW-L12)
关键词
人工智能
自动推理
扩展规则
碰集
CDP算法
CER算法
artificial intelligence
automated reasoning
extension rule
hitting set
CDP algorithm
CER algo rithm
