• 主题
高级搜索  >
历史搜索 清空历史
首页> 中文学位 >命题逻辑中随机3-SAT问题算法研究
【6h】

命题逻辑中随机3-SAT问题算法研究

代理获取
页面导航
  • 目录
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

目录

声明

摘要

第1章 绪论

1．1 研究背景和和研究意义

1．2 国内外研究现状

1．3 本文研究的内容和结构安排

第2章 基础知识

2．1 基本概念

2．2 符号说明

2．3 本章小结

第3章 4种SAT问题的算法介绍

3．1 SDF算法

3．2 Sparrow2011算法

3．3 ProbSAT算法

3．4 CCMC算法

3．5 本章小结

第4章 随机3-SAT问题新算法

4．1 初始赋值的优化

4．2 随机3-SAT问题新算法

4．3 子句权重重置函数

4．4 本章小结

第5章 算法评估

5．1 理论评估

5．2 测试标准

5．3 测试结果比较

5．4 本章小结

第6章 总结与展望

6．1 论文总结

6．2 展望

致谢

参考文献

附录

攻读硕士学位期间发表的论文及参与的科研工作

展开▼

摘要

命题逻辑公式的可满足性问题(SAT)是计算机科学和人工智能中一个重要问题。它是第一个被证明了的NP完全问题，由Stephen Cook于1971年提出。SAT问题在人工智能、软件工程、VLSI集成电路设计等领域具有广泛的应用。3-SAT问题是每个子句的文字个数固定为3的SAT问题。作为SAT问题的子问题之一，3-SAT问题也是NP完全问题。3-SAT问题有来自工业问题转化的实际问题，也有机器自动生成的。来自工业问题转化的3-SAT问题在数目和结构上都有很大的限制，根本不能满足各类SAT算法的测试需求，所以目前大部分的3-SAT问题来自机器自动生成，这类问题又称为随机3-SAT问题。当变元的数目达到1000乃至1兆的规模时，3-SAT问题的求解变得异常困难，所以对大规模随机3-SAT的求解是一个比较有前景的研究领域。
　　自从20世纪80年代随机3-SAT问题被提出以来，很多学者在这方面做了大量的工作，提出了各种各样的算法。当前较为高效的算法有Sparrow2011算法、ProbSAT算法、CCMC算法等。然而这些算法，在求解较大规模的随机3-SAT问题上的效率仍不够理想。
　　本文在综合分析以往SAT问题算法的基础上，在提高随机3-SAT问题的求解效率方面主要做了如下工作:
　　1、基于SAT问题的自身结构，研究各个文字在子句集中出现的频率，挖掘出文字与子句集可满足性判定的关系。给出文字的关键度和关键文字的概念，利用关键文字规则和DPLL规则设计出了对子句集初始真值指派的优化策略。
　　2、给出了基于优化后的初始真值指派的新的WASAT算法，算法先是运用真值指派综合评估函数来寻求更优的赋值，然后运用子句权重重置的策略，跳出局部最优解开辟新的搜索区域。
　　3、运用来自SAT竞赛网站的不同规模的随机3-SAT实例设计实验并得出结果。通过对比Sparrow2011算法、ProbSAT算法、CCMC算法，评估并分析了新的权重分析算法的效率。

著录项

相似文献

  • 中文文献
  • 外文文献
  • 专利
代理获取

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号