《中国科学院研究生院（计算技术研究所）》1997年硕士论文

发布时间：2016-07-04 22:01

  本文关键词：人工智能视野下的进化逻辑研究，由笔耕文化传播整理发布。

《中国科学院研究生院（计算技术研究所）》 1997年

命题逻辑的可满足性问题：复杂性和算法

卜东波  

【摘要】：可满足性问题(Satisfiablity问题)在数理逻辑、人工智能、机器学习、约束满足问题、VLSI集成电路设计与检测以及计算机科学理论等等领域具有广阔的应用背景。可满足性问题是第一个NP-Complete问题，并且是一大类NP-Complete问题的核心。大量的实践表明，，许多NP-Complete问题无论是对于计算机科学理论还是工程应用都有着至关重要的意义。可满足性问题的重要性以及它的一些奇妙的性质促使我们从问题和算法两个角度来研究它。 我们主要从问题本身的固有性质和快速求解算法两个角度来研究可满足性问题。值得注意的是：这两方面的研究工作是相辅相成、互相促进、互相启发的。从问题的角度，我们着重研究可满足性问题的相变现象以及问题实例的难度。这方面的工作更加清晰地刻划出问题本身的固有属性，从而有助于对问题的完整认识和合理分类，并且针对于各个不同的问题子类可以开发出更有效的算法。从算法的角度，我们分析了完备性算法和不完备性算法的复杂性，比较了两者的优缺点和适用范围，进而提出了将以上两种算法更加完美的结合的思想。我们提出的算法CCSAT和USAT，即分别针对于利用不完备性算法为完备性算法提供更强的启发式信息和利用完备性算法帮助不完备性算法处理局部极值点两个方向的结合。通过重新认识2SAT∈P这一结论证明的实质，也给算法的设计提供了新的思路。 问题的复杂性是问题的一个固有属性。我们试图用难度这个概念来描述和刻划它，并且给出了难度的一个新的、形式化定义的猜想。自然界中的物质皆有其物态和相，以及随系统序参数而发生的物质从一个相到另一个相的相变现象。作为一个复杂的计算系统，可满足性问题也有一个奇妙的相变现象，即问题实例的可满足概率随着实例的特定序参量的变化而发生的突变现象。我们提出了一种布尔筛模型，更加清晰地描述出相变现象。 我们主要做了以下8项工作，分为问题性质剖析类(标记为“P”)和

【关键词】：
【学位授予单位】：中国科学院研究生院（计算技术研究所）
【学位级别】：硕士
【学位授予年份】：1997
【分类号】：TP18
【目录】：

摘要4-7

Abstract7-12

第一章 引言12-16

1.1 NP-Complete问题和可满足性问题12-13

1.2 算法的优劣：收敛性和复杂性13-14

1.3 论文概要14-16

第二章 可满足性问题综述16-32

2.1 可满足问题的表示16-17

2.2 求解SAT问题的算法17-27

2.2.1 完备性算法18-23

2.2.2 局部搜索算法(Local Search)23-27

2.3 相变现象27-32

2.3.1 物理学中的相变现象27-30

2.3.2 可满足性问题中的相变现象30-32

第三章 相变现象和难度32-48

3.1 3-SAT问题可满足概率的布尔筛模型32-37

3.2 2-3-SAT问题的可满足概率37-39

3.3 相变现象的统计描述39-45

3.3.1 可能解的个数的期望值39-44

3.3.2 相变点上界的估计44-45

3.4.总结45

3.5 进一步的讨论45-48

第四章 可满足性问题的求解算法48-67

4.1 完备性算法和不完备性算法的比较48-49

4.2 求解SAT问题的完备性算法—CCSAT(Conflicted Cycle SAT)49-55

4.2.1 Crawford方案的剖析和CCSAT算法的提出49-52

4.2.2 mom策略的缺陷52-53

4.2.3 无级重排53-54

4.2.4.实验数据54-55

4.3 求解SAT问题算法的统一模型USAT(Uniform SAT)55-60

4.3.1 GSAT算法的特点及子空间旋转策略的引入55-56

4.3.2 统一的算法模型USAT56-58

4.3.3 实验数据58-59

4.3.4 总结59-60

4.4 求解SAT问题的第三类算法—概率性算法60-62

4.5 完备性算法APTSAT(Avoid Phase Transition SAT)62-64

4.5.1 子问题的又一种分类方法63

4.5.2 完备性算法APTSAT63-64

4.6 新的剪枝规则：Subset-Prune剪枝64-67

4.6.1 求解2-SAT问题的P算法64-66

4.6.2 Subset-Prune剪枝规则66-67

第五章 结束语67-68

参考文献68-71

硕士期间发表的论文71-72

作者简历72

下载全文 更多同类文献

CAJ全文下载

(如何获取全文？ 欢迎：购买知网充值卡、在线充值、在线咨询)

CAJViewer阅读器支持CAJ、PDF文件格式

【参考文献】

中国期刊全文数据库 前3条

1 李未,黄文奇;一种求解合取范式可满足性问题的数学物理方法[J];中国科学(A辑 数学 物理学 天文学 技术科学);1994年11期

2 黄文奇,金人超;求解SAT问题的拟物拟人算法—Solar[J];中国科学E辑:技术科学;1997年02期

3 白硕,卜东波;2-3-SAT问题相变现象剖析及其应用[J];软件学报;1998年11期

【共引文献】

中国期刊全文数据库 前10条

1 张晓君;;为什么语言学研究离不开逻辑学——2009语言学和逻辑学交叉研究研讨会侧记[J];毕节学院学报;2010年05期

2 刘云翔,孙吉贵;模糊集合的语义[J];长春工程学院学报(自然科学版);2003年03期

3 邓安生,关伟洲;布尔算子模糊逻辑中的广义半锁归结原理[J];东北师大学报(自然科学版);2000年03期

4 邓安生;布尔算子模糊逻辑中的删除策略[J];东北师大学报(自然科学版);1998年01期

5 胡勤;;人工智能概述[J];电脑知识与技术;2010年13期

6 刘富春;;再扩充模糊逻辑中归结方法的有效性[J];广东工业大学学报;2006年01期

7 邓苏,张维明,陈文伟,陈卫东,汤大权;软试验床关键技术——知识获取及管理系统[J];国防科技参考;1995年01期

8 滕至阳,袁全生,程正潮;分割图描述的正确性验证[J];高技术通讯;1998年04期

9 赵天玉;组合优化算法中摆脱局部极小值的几种策略[J];工科数学;2000年01期

10 万良;;随机填充问题与排课系统[J];贵州教育学院学报;2007年02期

中国重要会议论文全文数据库 前3条

1 黄文奇;陈端兵;;用纯粹拟人型算法求解超大规模集成电路布局中的矩形packing问题[A];2005年全国理论计算机科学学术年会论文集[C];2005年

2 赖家俊;潘小东;徐开俊;徐扬;;基于十八元非链格值命题逻辑L_(18)P(X)中的归结方法的研究[A];第六届中国不确定系统年会论文集[C];2008年

3 于津;刘叙华;;基于不确定、不精确知识的推理系统-UKRS[A];1996年中国智能自动化学术会议论文集（上册）[C];1996年

中国博士学位论文全文数据库 前10条

1 周俊萍;自动推理与规划问题最小上界和相变规律研究[D];吉林大学;2011年

2 胡明娣;逻辑度量空间的内蕴结构的研究[D];陕西师范大学;2011年

3 邹丽;基于语言真值格蕴涵代数的格值命题逻辑及其归结自动推理研究[D];西南交通大学;2010年

4 熊正大;链式几何结构的拟人型优化方法[D];华中科技大学;2011年

5 黄越;数字集成电路自动测试生成算法研究[D];江南大学;2012年

6 赵孝武;求解正交表问题的拟物拟人方法[D];中国科学院软件研究所;2001年

7 赵光峰;格蕴涵代数与图的升分解问题的研究[D];西南交通大学;2002年

8 马骏;基于格蕴涵代数的格值逻辑系统及其自动推理的研究[D];西南交通大学;2002年

9 斐峥;基于神经网络的自动推理理论及方法的研究[D];西南交通大学;2002年

10 汤永川;关于不确定性推理理论与知识发现的研究[D];西南交通大学;2002年

中国硕士学位论文全文数据库 前10条

1 刘文赫;Horn子句型信念的静态非修正处理方法研究[D];大连海事大学;2011年

2 周国城;求解圆形Packing问题及模型蛋白结构预测问题的启发式算法[D];南京信息工程大学;2011年

3 陈稳;基于DPLL的SAT算法的研究及应用[D];电子科技大学;2011年

4 金宏妍;人工智能视野下的进化逻辑研究[D];燕山大学;2010年

5 倪海文;团簇基态结构预测的高效启发式算法[D];华中科技大学;2011年

6 黄冲;组合优化中的命题逻辑[D];华中科技大学;2011年

7 汪轲;无线传感网络覆盖控制策略的研究[D];浙江师范大学;2011年

8 吴瑕;布尔算子模糊逻辑中的调解法[D];东北师范大学;2002年

9 高燕;基于数据挖掘技术的海关执法评估系统的研究与开发[D];武汉理工大学;2002年

10 王宏川;因果图推理及其应用研究[D];重庆大学;2002年

【二级参考文献】

中国期刊全文数据库 前6条

1 黄文奇,陈亮;求解有关空间利用的调度问题的拟物方法[J];中国科学(A辑 数学 物理学 天文学 技术科学);1991年03期

2 李未;一个开放的逻辑系统[J];中国科学(A辑 数学 物理学 天文学 技术科学);1992年10期

3 李未,黄文奇;一种求解合取范式可满足性问题的数学物理方法[J];中国科学(A辑 数学 物理学 天文学 技术科学);1994年11期

4 黄文奇;求解Covering问题的拟物方法——NP难度问题的一个处理途径[J];计算机学报;1989年08期

5 黄文奇,朱虹,许向阳,宋益民;求解方格packing问题的启发式算法[J];计算机学报;1993年11期

6 黄文奇,詹叔浩;求解Packing问题的拟物方法[J];应用数学学报;1979年02期

【相似文献】

中国期刊全文数据库 前10条

1 徐小萍;;MARG-MU(2)的结构和复杂度[J];井冈山学院学报;2009年02期

2 张德富;求解难可满足性问题的混合算法[J];小型微型计算机系统;2003年08期

3 丁敏;唐璞山;;改进的时间帧展开的时序电路等价验证算法[J];计算机辅助设计与图形学学报;2006年01期

4 张忠林;唐璞山;;一个基于可满足性算法的时序深度计算方法[J];计算机工程;2006年02期

5 苏俊霞;;社会认识优化在非线性规划问题中的应用[J];计算机仿真;2007年09期

6 毕忠勤;陈光喜;单美静;;可满足性问题全部解的求解算法[J];计算机工程与应用;2009年03期

7 王建新;管利娜;江国红;;可满足性问题的研究综述[J];计算技术与自动化;2009年04期

8 吴耀辉;梁丰;蔡宇;;基于SystemC的SAT求解器设计[J];电脑知识与技术;2010年14期

9 余丰人;丘海明;;关于合取范式可满足性问题的复杂性分析[J];中山大学学报(自然科学版);2006年02期

10 荆明娥;陈更生;赵长虹;唐璞山;周电;;利用正交方法解SAT问题[J];复旦学报(自然科学版);2008年06期

中国重要会议论文全文数据库 前1条

1 熊伟;唐璞山;;一种新的SAT问题预处理算法[A];2007年全国开放式分布与并行计算机学术会议论文集(下册)[C];2007年

中国博士学位论文全文数据库 前10条

1 丁敏;可满足性问题算法研究以及在时序电路等价验证中的应用[D];复旦大学;2005年

2 杨军;集成电路的逻辑等价性验证研究[D];浙江大学;2007年

3 翁延玲;RTL到门级设计的等价性验证的研究[D];浙江大学;2008年

4 沈静;约束满足问题的模型构造和相变现象[D];华中师范大学;2011年

5 郑飞君;基于布尔可满足性的逻辑电路等价性验证和测试生成技术研究[D];浙江大学;2008年

6 许有军;基于扩展规则的若干SAT问题研究[D];吉林大学;2011年

7 张立明;结合可满足的基于模型等价性验证及不一致诊断问题研究[D];吉林大学;2012年

8 曾国强;改进的极值优化算法及其在组合优化问题中的应用研究[D];浙江大学;2011年

9 汪隽;受生物启发的脉冲神经膜系统的计算能力研究[D];华中科技大学;2013年

10 黄玉芳;算法Tile自组装系统的设计与应用研究[D];华中科技大学;2010年

中国硕士学位论文全文数据库 前10条

1 江智兰;DNA计算模型研究与探索[D];安徽理工大学;2013年

2 王霄维;应用于集成电路形式化验证的SAT算法研究[D];长春工业大学;2010年

3 傅琳璐;基于分支回溯的NAE-3SAT及#NAE-3SAT问题求解算法[D];东北师范大学;2013年

4 宋勃升;DNA自组装计算模型的应用研究[D];安徽理工大学;2011年

5 黄劲楠;可满足性问题算法研究-CNF的简化[D];复旦大学;2008年

6 姚尧;基于回归分析和DCM模型的可满足性问题求解算法[D];东华大学;2011年

7 赵松云;基于子句权重求解SAT问题[D];复旦大学;2008年

8 赵伟楠;对可满足性（SAT）问题求全解的算法研究及实现[D];北京交通大学;2009年

9 王全新;量子进化算法改进及应用研究[D];吉林大学;2007年

10 陈稳;基于DPLL的SAT算法的研究及应用[D];电子科技大学;2011年

  本文关键词：人工智能视野下的进化逻辑研究，由笔耕文化传播整理发布。

本文编号：66062