基于扩展规则的启发式#SAT求解算法

• 作者: 刘磊 吕帅 王强
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 扩展规则 模型计数 启发式算法 极大项空间 规约子句
• 年，卷（期）: 2018,（11）
• 所属期刊栏目: 模式识别与人工智能
• 页码范围: 3517-3527
• 页数: 11页
• 分类号: TP181
• 字数: 8337字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005298

摘要

#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究,发现选择规约子句的顺序对极大项空间的大小有着较大的影响,因此提出两种加速#SAT求解的启发式策略:MW和LC&MW.MW每次选择具有最大权值的子句作为规约子句;LC&MW每次选择最长子句作为规约子句,若最长子句存在多个,则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CER_MW,利用LC&MW策略设计了算法CER_ LC&MW.实验结果表明,CER MW和CER LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面,CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍～100倍.在求解能力方面,CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘磊	吉林大学计算机科学与技术学院	211	1231	18.0	25.0