学位论文 > 优秀研究生学位论文题录展示

基于回归分析和DCM模型的可满足性问题求解算法

作　者: 姚尧
导　师: 陈镜超
学　校: 东华大学
专　业: 模式识别与智能系统
关键词: 可满足性问题 SAT求解器回归分析模型 DCM模型
分类号: TP301.6
类　型: 硕士论文
年　份: 2011年
下　载: 26次
引　用: 0次
阅　读: 论文下载

内容摘要

可满足性问题是第一个NP完全问题,在计算机辅助设计、人工智能、密钥攻击、电子设计自动化、规划等领域有着广泛的应用。目前还没有一个SAT求解器可以有效求解所有SAT问题,仍有大量的问题未被解决。SAT求解器大致可以分为两大类：一类是基于DPLL的；另一类是基于局域搜索的。基于DPLL的SAT求解器又可以进一步分成前向型和冲突驱动型两种。其中前向型在求解随机类不可满足性问题和手工类问题上表现出色,冲突驱动型在求解应用类问题上占据主导,而基于局域搜索的在求解大的随机类可满足性问题上表现很好。由于不同求解器擅长求解不同的问题,本文引入了轮廓特征的策略。希望通过模型寻找最优求解器的思路构造出一种通用性的SAT求解器。其中回归分析模型建立了实例特征和求解器执行时间的关系,计算出待解问题的特征就可以估算出其执行时间,进而选择执行时间最短的求解器作为最优求解器去求解。DCM模型以求解器的行为作对象,执行输出作特征,求解出每个求解器的执行概率,从而选择执行概率最大的求解器作为最优求解器去求解。最后将回归分析模型和DCM模型相结合,先由回归分析模型粗选出一组较优求解器,再由DCM模型细选出其中执行概率最大的作为最优求解器去求解。实验表明轮廓特征算法可明显提高了SAT求解器的解题数量。求解问题数量上混合模型大于DCM模型,DCM模型大于回归分析模。再从执行时间上看,对于简单的问题,混合模型和回归分析模型相当,都优于DCM模型,对于复杂的问题,混合模型和DCM模型相当,都优于回归分析模型。总体上讲混合模型集成了两种模型的优点,无论从解题数量还是执行时间上看,它都略胜于前面两者。

全文目录

摘要  5-7
ABSTRACT  7-11
第1章可满足性问题的背景  11-16
  1.1 可满足性问题的定义  11-12
  1.2 可满足性问题的研究现状  12-13
  1.3 可满足性问题的应用及意义  13-16
第2章可满足性问题的各种求解算法  16-28
  2.1 DPLL算法  16-26
    2.1.1 冲突驱动型DPLL算法  16-21
    2.1.2 前向型DPLL算法  21-26
  2.2 局部搜索算法  26-27
  2.3 轮廓特征求解算法  27-28
第3章基于回归分析的求解算法  28-32
  3.1 回归分析算法  28-29
  3.2 回归分析模型求解器的构造  29-32
第4章基于DCM模型的求解算法  32-35
  4.1 DCM模型结构  32-33
  4.2 DCM模型求解器的构造  33-35
第5章两种模型混合的求解算法  35-37
  5.1 两种模型混合算法  35-36
  5.2 两种模型混合求解器的构造  36-37
第6章实验研究  37-41
  6.1 试验环境  37
  6.2 试验结果分析  37-41
第7章总结展望  41-43
  7.1 轮廓特征求解算法的总结  41
  7.2 未来研究工作展望  41-43
参考文献  43-47
附录1 回归分析模型的回归系数  47-48
作者在研究生期间的研究成果  48-49
致谢  49

基于回归分析和DCM模型的可满足性问题求解算法

内容摘要

全文目录

相似论文