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

摘要：

为解决可满足性(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％.

关键词：SAT问题、启发式算法、搜索算法、变量决策、演绎推理

所属期刊栏目：52

分类号：TP311.1(计算技术、计算机技术)

资助基金：国家自然科学基金资助项目61673320,11526171,61305074;中央高校基本科研业务费专项资金资助项目2682017ZT12

在线出版日期：2018-01-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1224-1232