利用逻辑演绎求解SAT问题的启发式完全算法

• 作者: 何星星 徐扬 陈青山
• 来源期刊: 西南交通大学学报
• 学科: 工学
• 关键词: SAT问题 启发式算法 搜索算法 变量决策 演绎推理
• 年，卷（期）: 2017,（6）
• 页码范围: 1224-1232
• 页数: 9页
• 分类号: TP311.1
• 字数: 7195字
• 语种: 中文
• DOI: 10.3969/j.issn.0258-2724.2017.06.025

摘要

为解决可满足性(satisfiability problem,SAT)问题求解过程中分支决策效率不高的问题,提出了一种基于逻辑演绎分组(logical deduction group,LDG)的启发式完全算法.该算法通过选择剩余未满足子句参与逻辑演绎,得到一组局部可满足赋值序列,并引导求解器优先搜索赋值序列所在解空间;对于可满足问题,可以通过迭代调用演绎过程,将局部可满足解成组地扩充为全局可满足解,对于不可满足问题,如果演绎结果出现空子句,则可以直接判定.采用SAT国际竞赛的实例,与具有代表性的指数级变元状态独立下降和(exponential variable state independent decaying sum,EVSIDS)变量决策算法进行了对比测试,结果表明:在求解总问题数方面,LDG比EVSIDS多出42个;在求解速度方面,LDG对可满足问题的求解时间相较EVSIDS平均减少了22.8％,对不可满足问题的求解时间平均减少了17.8％,总平均时间减少了20.1％.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐扬	西南交通大学系统可信性自动验证国家地方联合工程实验室	186	1462	15.0	32.0
2	何星星	西南交通大学系统可信性自动验证国家地方联合工程实验室	12	35	3.0	5.0
3	陈青山	西南交通大学信息科学与技术学院	3	7	1.0	2.0