可满足问题求解算法DPLL的优化技术研究

摘要

求解效率一直是可满足性问题(SAT)的研究热点，因为提高效率可以有效的扩大SAT的应用范围。长期以来，研究者们对此进行了不断地探索，并提出了多种算法，如Tableau、DPLL、GRASP等。随着研究的进一步深入，人们发现DPLL算法具有高效、易操作等优点，所以对DPLL算法的优化与改进逐渐成为SAT求解算法的核心。本文在DPLL算法的基础上，针对它在选取判定变量时过于随机的问题，提出了两种判定层优化技术。具体研究内容如下:
　　1、提出了基于变量个数的判定启发式策略。该策略是在对DPLL完备算法的学习和不同形式下对子句文字排序处理研究的基础上提出的，它通过统计子句集中每个变量的出现次数，并考虑变量中正负文字的出现次数，然后挑选出次数最高的进行赋值。实例结果表明，应用该策略求解时可以有效简化实例的求解空间，减少求解步骤，尽早剪除不满足解空间，从而有效提高求解效率。
　　2、提出了基于文字分数的判定启发式策略。该策略是在考虑子句长短和变量正负出现对变量判定影响的基础上提出的，它通过对子句集中每一个文字设定一个分数，并将分值高的作为判定变量，同时在求解过程中，及时删除已满足子句。实例结果表明，该策略的提出有利于提高判定变量选取的准确性，可以有效避免一定的冲突，降低求解时间，使得求解效率显著提高。

目录

声明

摘要

1 绪论

1．1 研究背景及意义

1．2 国内外研究现状

1．3 本文工作

1．4 文章结构

2 SAT问题及其求解算法

2．1 SAT问题

2．2 SAT算法

3 DPLL算法

3．1 预备知识

3．2 抽象的DPLL算法

3．2 经典的DPLL系统

3．3 现代的DPLL系统

4 DPLL算法判定层优化技术

4．1 判定层启发式概述

4．2 基于变量个数的判定启发式策略

4．3 基于文字分数的判定启发式策略

4．4 实例对比

结论

参考文献

攻读硕士学位期间发表学术论文情况

致谢