基于蕴含推理的SAT预处理器的实现

发布时间：2020-08-02 11:00

【摘要】： 可满足问题(SAT)是第一个被证明的NP-完全问题[Cook71],是Johnson等人在上千个NP问题中总结出的六个最具代表性的问题之一,它在计算复杂性理论中具有极其重要的地位,其理论研究三十多年来从未停止过。可满足问题在人工智能、集成电路设计、规划、图论等重要领域中都有所应用(存在直接的可满足问题或者可以转化为可满足实例高效求解的问题),同时,由于该问题描述和数据表示非常简单,因此是很好的算法试验田,从这里发展出的算法技术可以快速的应用于其他问题上。因此,高效实用的可满足算法设计与分析同样是多年来的研究热点。 本文的研究工作是针对可满足问题的预处理问题展开的,预处理是对求解问题进行简化,以实现帮助问题求解的目的。本文首先分析和介绍了可满足问题算法一路走来过程中衍生出的几种经典算法,以及预处理方面的几种常见算法。针对其中的预处理工作提出了改进的方法,并实现提高整个问题解决效率的目的。 本文主要的价值之处在于：(1)使用二元关系矩阵来构建逻辑蕴含图,使用映射关系辅助进行逻辑蕴含关系的推导；(2)结合高级逻辑推导技术以及逻辑蕴含图的对称性推进简化过程。从实验分析表明,这些措施能够有效地提高解决可满足问题的效率,并在一些情况下能够独立发现问题是否可满足。
【学位授予单位】：复旦大学
【学位级别】：硕士
【学位授予年份】：2009
【分类号】：TP332

【相似文献】

相关期刊论文 前10条

1 黄庆华;;Oracle专题——外连接过滤[J];数字技术与应用;2011年08期

2 殷明浩;周俊萍;孙吉贵;谷文祥;;求解QBF问题的启发式调查传播算法[J];软件学报;2011年07期

3 邢赜聪;;SQL案例专题-缺勤者[J];数字技术与应用;2011年08期

4 杨振宇;;巧用SQL的查询技术[J];软件;2011年04期

5 崔宝合;王秋华;;信息管理与信息系统在医院的应用[J];企业导报;2011年12期

6 宋勃升;殷志祥;甄诚;华程;;DNA自组装的可满足性问题模型[J];小型微型计算机系统;2011年09期

7 张桂燕;;基于数据库的语句优化经验之谈[J];电脑知识与技术;2011年17期

8 韩竞锋;;数据库应用系统性能优化研究与实践[J];信息安全与技术;2011年06期

9 梁凤萍;;浅析数据库查询优化[J];大众标准化;2011年S1期

10 盘青梅;;大型表SQL查询的优化与用户编写策略[J];太原城市职业技术学院学报;2011年08期

相关会议论文 前10条

1 赵英阳;许道云;;NT-HIT(k)公式的存在性[A];2005年全国理论计算机科学学术年会论文集[C];2005年

2 蒋志华;姜云飞;;一种构造Prolog程序子句本体的方法(英文)[A];全国语域web与本体能研讨会论文集[C];2006年

3 文卫平;;英汉驴子句的差异[A];中国英汉语比较研究会第八次全国学术研讨会论文摘要汇编[C];2008年

4 魏振春;汪国胜;毕翔;刘小平;;规则化描述方法中的规则化简方法[A];全国第20届计算机技术与应用学术会议（CACIS·2009）暨全国第1届安全关键技术与应用学术会议论文集（上册）[C];2009年

5 邵明;李光辉;李晓维;;提取极小布尔不可满足子式[A];全国第13届计算机辅助设计与图形学（CAD/CG）学术会议论文集[C];2004年

6 刘新;;10FL中(μ,ν)-归结原理的完备性[A];模糊集理论与模糊应用专辑——中国系统工程学会模糊数学与模糊系统委员会第十届年会论文选集[C];2000年

7 廖加彬;林世平;;基于聚类的中文浅层语义模式识别[A];中国电子学会第十五届信息论学术年会暨第一届全国网络编码学术年会论文集（下册）[C];2008年

8 练睿婷;史晓东;;语篇标注语料库的建设研究[A];第四届全国学生计算语言学研讨会会议论文集[C];2008年

9 高印芝;黄冬梅;;关于Fuzzy逻辑函数的性质的进一步讨论[A];模糊集理论与应用——98年中国模糊数学与模糊系统委员会第九届年会论文选集[C];1998年

10 陈敏;;应用DCG文法分析汉语[A];语言文字应用研究论文集（Ⅰ）[C];1995年

相关重要报纸文章 前10条

1 贵州 王伟;用ORDER BY子句排序[N];电脑报;2004年

2 贵州 王伟;用GROUPBY子句分组[N];电脑报;2004年

3 邱晓理;Oracle数据库系统性能优化策略[N];计算机世界;2006年

4 河南 张华贵;数据库中参数化查询的实现[N];电脑报;2001年

5 ;检阅DB2 Viper[N];计算机世界;2006年

6 山东 任立群;深挖SQL语句潜力查询效率自然高[N];电脑报;2004年

7 王珂;你想的才是你要的[N];中国电脑教育报;2002年

8 ;实例破解Flash[N];电脑报;2001年

9 Warton;Java的异常处理[N];电脑报;2004年

10 逍遥;用SQL实现树的查询[N];计算机世界;2002年

相关博士学位论文 前10条

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

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

3 王秀芹;基于SAT的数字电路形式验证方法研究[D];哈尔滨工程大学;2009年

4 吕帅;基于自动推理技术的智能规划方法研究[D];吉林大学;2010年

5 石振国;资源网络的精化学习及应用研究[D];上海大学;2011年

6 刘全;基于tableau的自动推理研究[D];吉林大学;2004年

7 于鹏;统计关系模型学习方法的研究[D];吉林大学;2008年

8 古华茂;描述逻辑概念可满足性推理研究[D];浙江大学;2009年

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

10 许中卫;基于双向搜索的ILP算法构建汉语语义自动切分系统[D];安徽大学;2006年

相关硕士学位论文 前10条

1 傅阳春;基于2-SAT求解器的SAT算法研究[D];华南理工大学;2010年

2 霍翔;SMT求解器增强技术的研究[D];北京交通大学;2011年

3 冯陆;子句型信念集静态非修正处理方法的优化研究[D];大连海事大学;2012年

4 咸爱勇;合取范式最大不全满足与最大可满足问题的局部搜索算法研究[D];山东大学;2012年

5 杜巧霞;子句主语的英汉对比研究[D];湖南大学;2012年

6 赵英阳;NT-HIT公式的存在性[D];贵州大学;2006年

7 王迪海;一类SAT Benchmark的算法研究及其应用[D];电子科技大学;2010年

8 李淑霞;基于局部搜索隐蔽集算法的QBF求解器研究[D];东北师范大学;2010年

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

10 刘雷;纵览传播算法求解随机3-SAT问题[D];吉林大学;2010年

本文编号：2778422