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

对可满足性（SAT）问题求全解的算法研究及实现

作　者: 赵伟楠
导　师: 吴为民
学　校: 北京交通大学
专　业: 计算机科学与技术
关键词: 可满足性问题 全解求解器 增量式 隔离子句
分类号: TP301.6
类　型: 硕士论文
年　份: 2009年
下　载: 224次
引　用: 3次
阅　读: 论文下载
 

内容摘要


可满足性问题(satisfiability problem,简称SAT问题)作为第一个被证明的NP完全问题,有着重要的理论及应用意义。它是计算机理论与应用的核心问题,在计算机科学、人工智能等学科中有重要的理论及应用价值。而对可满足性问题求全解,在电子设计自动化(Electronic Design Automation,简称EDA)领域有着重要的应用价值。本文介绍了对可满足性问题求全解的理论及实践意义。对可满足性求解器算法进行比较,从中选择了效率较高且适用于全解求解器的算法。分别从增量式和隔离子句的角度,提出了两点适用于全解求解器的新算法:(1)从增量式角度对文字权值进行调整,并提出对隔离子句的冲突分析及回溯处理。本算法结合了布尔可满足性程序中的变量状态独立衰减总和的启发式决策算法,对于全解求解器运行过程中加入的隔离子句所涉及的文字权值进行调整,从而提高全解求解效率。对隔离子句造成的冲突提出专门的冲突分析及回溯处理机制,使每次添加一个隔离子句后,程序可以迅速进入下一次求解过程。(2)从隔离子句的角度对全解求解器进行改进。提出了基于CNF的类Don’tcares算法。这一算法借鉴了基于混合表示法(hybrid representations,即将电路特征和合取范式相结合)的Don’t cares算法,提出了单纯基于合取范式输入法的类Don’t cares算法。使基于CNF输入的全解求解器效率得到了一定程度的提高。提出对隔离子句的归并处理策略。能够对当前得到的隔离子句进行一定程度的归并处理,又不需要消耗太多的运行时间和系统空间资源。从实验结果可以看出以上两种算法对全解求解器效率的提高。

全文目录


致谢  5-6
中文摘要  6-7
ABSTRACT  7-10
1 综述  10-17
  1.1 课题研究意义  10-12
    1.1.1 理论意义  10
    1.1.2 应用意义  10-12
  1.2 对可满足性问题求全解  12-13
  1.3 国内外研究现状  13-14
  1.4 论文主要工作及内容安排  14-17
    1.4.1 主要工作  14-15
    1.4.2 内容安排  15-17
2 可满足性求解器的实现  17-34
  2.1 DPLL算法框架  17-19
    2.1.1 原始DPLL算法  17-18
    2.1.2 改进的DPLL算法  18-19
  2.2 启发式算法  19-22
    2.2.1 传统启发式算法  19-20
    2.2.2 变量状态独立衰减总和的启发式决策算法  20-22
  2.3 布尔约束传播算法  22-27
    2.3.1 一些布尔约束传播算法  22-24
    2.3.2 双文字监视算法  24-27
  2.4 冲突学习算法  27-32
    2.4.1 蕴含关系图  27-28
    2.4.2 冲突分析和学习机制  28-31
    2.4.3 各种分割学习算法及其比较  31-32
  2.5 实验结果  32-34
3 从增量式角度提高全解求解效率  34-45
  3.1 对可满足性求解器的算法改变  34-37
    3.1.1 隔离子句  34-36
    3.1.2 内存问题  36-37
  3.2 全解求解器的基本算法实现  37-39
    3.2.1 可满足性求解器算法  37-38
    3.2.2 全解求解器的基本算法  38-39
  3.3 增量式求解  39-43
    3.3.1 基本概念  39
    3.3.2 文字权值调整  39-40
    3.3.3 冲突分析及回溯处理  40-43
  3.4 实验结果及分析  43-45
4 对隔离子句的算法改进  45-57
  4.1 类Don't cares算法  45-51
    4.1.1 Don't cares算法思想  45-48
    4.1.2 基于CNF的类Don't cares算法  48-51
  4.2 对隔离子句的归并  51-53
  4.3 低内存条件下的算法  53
  4.4 实验结果及分析  53-57
5 总结与展望  57-60
  5.1 全文工作总结  57-58
  5.2 研究展望  58-60
参考文献  60-62
作者简历  62-64
学位论文数据集  64

相似论文

  1. 全球化背景下当代中国发展道路研究,D616
  2. 单元机组协调控制系统建模与优化及其对电网稳定性的影响,TM621.3
  3. 开源软件依赖可满足性识别方法研究与实现,TP311.52
  4. DNA自组装计算模型的应用研究,O242.1
  5. 基于进化非选择算法的可满足性问题求解,TP18
  6. 纵览传播算法求解随机3-SAT问题,TP18
  7. 基于回归分析和DCM模型的可满足性问题求解算法,TP301.6
  8. 基于DPLL的SAT算法的研究及应用,TP301.6
  9. 可满足性问题算法研究-CNF的简化,TP301.6
  10. 基于子句权重求解SAT问题,TN402
  11. 一种新的基于扩展规则的知识编译方法,TP182
  12. 离散数学中NP完全问题的DNA计算,TP301.6
  13. 基于SAT的VLSI测试向量自动生成技术,TN402
  14. 可满足性问题和图染色的一些研究,TP301.6
  15. 数据挖掘中的关联规则发现,TP311.13
  16. 命题逻辑的可满足性问题：复杂性和算法,TP18
  17. 量子进化算法改进及应用研究,TP301.6
  18. 满足性算法在形式化验证中的应用研究及实现,TP301.6
  19. 一阶逻辑模型搜索问题研究,TP301.6
  20. 一种改进的DNA计算模型研究,TP301

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 一般性问题 > 理论、方法 > 算法理论
© 2012 www.xueweilunwen.com