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

发布时间：2018-07-24 17:21

【摘要】：为解决可满足性(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%.
[Abstract]:A heuristic complete algorithm based on logical deductive grouping (logical deduction) is proposed to solve the problem of low branch decision efficiency in the process of solving satisfiability problem. By selecting remaining unsatisfied clauses to participate in logical deduction, the algorithm obtains a set of locally satisfiable assignment sequences, and leads the solver to search the solution space of assignment sequences first. The locally satisfiable solution is extended to a global satisfiable solution in groups. For the unsatisfiable problem, if there is an empty subsentence in the deductive result, it can be judged directly. An example of SAT international competition is used to compare it with the representative exponential variable state independent descent and (exponential variable state independent decaying sum EVSIDS variable decision making algorithm. The results show that there are 42 more LDGs than EVSIDS in solving the total number of problems. In terms of solving speed, the average time for solving satisfiable problems is 22.8 less than that for EVSIDS, the average time for solving unsatisfiable problems is 17.8, and the total average time is 20.1.
【作者单位】：西南交通大学信息科学与技术学院;西南交通大学系统可信性自动验证国家地方联合工程实验室;
【基金】：国家自然科学基金资助项目(61673320,11526171,61305074) 中央高校基本科研业务费专项资金资助项目(2682017ZT12)
【分类号】：TP301.6

【相似文献】