检索结果-内蒙古大学图书馆

您好，读者！请登录

内蒙古大学图书馆

首页
概况
党建
资源
服务
科研支持
- 论文收录引用证明
- 科技查新
知识产权
档案馆
帮助

咨询与建议

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

您的常用邮箱：*

您的手机号码：*

问题描述：

当前已输入0个字，您还可以输入200个字

全部搜索
期刊论文
图书
学位论文
标准
纸本馆藏
外文资源发现
数据库导航
超星发现

高级检索

时间限定

出版年份：

文献类型

图书期刊文献学位论文多媒体

馆藏选择

电子馆藏纸本馆藏

核心期刊

全部期刊 SCI 收录期刊 SSCI 收录期刊 EI 收录期刊 CSCD 收录期刊 CSSCI 收录期刊

语言

中文英文

文献类型

期刊文献图书学位论文标准纸本馆藏

帮助

文字说明：

T=题名（书名、题名），A=作者（责任者），K=主题词，P=出版物名称，PU=出版社名称，O=机构（作者单位、学位授予单位、专利申请人），L=中图分类号，C=学科分类号，U=全部字段，Y=年（出版发行年、学位年度、标准发布年）

检索规则说明：

AND代表“并且”；OR代表“或者”；NOT代表“不包含”；(注意必须大写,运算符两边需空一格)

检索范例：

范例一：(K=图书馆学 OR K=情报学) AND A=范并思 AND Y=1982-2016
范例二：P=计算机应用与软件 AND (U=C++ OR U=Basic) NOT K=Visual AND Y=2011-2016

分类表

所选分类

>> <<

限定检索结果

文献类型

4 篇 学位论文

馆藏范围

4 篇 电子文献
0 种 纸本馆藏

日期分布

学科分类号

3 篇 哲学
- 3 篇 哲学
3 篇 理学
- 3 篇 数学
1 篇 工学
- 1 篇 计算机科学与技术...
- 1 篇 软件工程

主题

4 篇 分支启发式策略
2 篇 cdcl算法
2 篇 sat问题
1 篇 智能回溯
1 篇 冲突分析
1 篇 dpll算法
1 篇 sat求解器
1 篇 cdcl sat求解器
1 篇 学习子句删除启发...
1 篇 bcp
1 篇 学习子句评估
1 篇 命题逻辑
1 篇 ldcr策略
1 篇 drb算法
1 篇 dpll
1 篇 sat
1 篇 学习子句管理策略

机构

3 篇 西南交通大学
1 篇 上海交通大学

作者

1 篇 焦加麟
1 篇 陈秀兰
1 篇 胡容
1 篇 孙菁

语言

4 篇 中文

检索条件"主题词=分支启发式策略"

共 4 条记录，以下是1-10 订阅

全选清除本页清除全部题录导出标记到"检索档案"

详细简洁

排序：

基于CDCL的SAT问题的分支启发式策略研究

基于CDCL的SAT问题的分支启发式策略研究

引用

作者：胡容西南交通大学

学位级别：硕士

命题逻辑公式的可满足性问题（SAT问题）是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全（Non... 详细信息

命题逻辑公式的可满足性问题（SAT问题）是指给出一个合取范式,判断是否存在一组赋值使得这个合取范式可满足。SAT问题是计算机科学与工程、人工智能、计算机视觉和计算机辅助设计等领域的一个核心问题,它也是第一个被证明的NP完全（Non-Deterministic Polynomial-Complete,NPC）问题。正因为如此,研究SAT问题并提高求解器的效率是很有价值的。求解SAT问题的算法分为完备算法和不完备算法。完备算法的特点是在问题可满足时,给出一个模型;不可满足时,给出证明。基于完备算法的优点,本文以CDCL（Conflict Driven Clause Learning,CDCL）算法为框架,研究CDCL算法的以下主要流程:决策、冲突分析、学习子句和回溯之间的关系。SAT求解器的成功绝大多数归因于从错误赋值中学习的能力、快速地删除搜索空间以及首先集中在那些“重要”变量中[1]。故本文集中在CDCL算法中的决策和冲突分析上,取得的主要研究结果如下:1.当一个命题逻辑中的逻辑公式以CNF的形式输入到数据库时,从中选择“重要”变量的依据是变量出现的次数和包含该变量子句的长度。因为越短的子句越难满足,故优先考虑短子句,相应地,短子句中的变量就“重要”。由这些信息,给出变量的初始计分和排序方法。2.当发生冲突时,即当前赋值使得某些子句为不可满足子句,参与冲突的那些子句中对应的变量的价值高于没有参与冲突的,因而在这个阶段考虑由这些子句或者变量所携带的信息刻画变量的贡献值。根据参考文献中的实验数据分析看出指数级的增长效果较好,因此,根据学习子句长度的不同,进行分段,在每个段,给出一个常数加上一个指数函数的方法进行计分排序。3.根据以上研究结果提出一种新的分支启发式策略并运用在glucose4.0算法上,用2016和2017年SAT竞赛例子和SATLIB例子测试,根据效果修改参数。结果表明在一定程度上比原始求解器glucose4.0有所提高。

关键词： SAT问题 DPLL算法 CDCL算法分支启发式策略

来源：评论

学校读者我要写书评

暂无评论

基于CDCL求解SAT问题的启发式策略研究

基于CDCL求解SAT问题的启发式策略研究

引用

作者：陈秀兰西南交通大学

学位级别：硕士

在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是... 详细信息

在逻辑问题中,布尔可满足性问题(即SAT问题)一直广受人们的关注。SAT问题是确定以合取范式(CNF)的形式给出的命题逻辑公式是否具有对其变量的一组布尔真值赋值,使得该公式是可满足的,或者证明它不可满足。SAT问题在算法时间复杂度上是首个被证明的NP完全问题。目前,SAT问题是许多领域的研究热点,如定理证明、自动推理、模型检查、电子设计自动化、计算机辅助设计等。因此,有关SAT问题的研究,不仅在理论方面意义重大,而且在实际应用中也有着巨大的价值。不完备算法和完备算法是解决SAT问题的两类主要算法。不完备算法主要基于随机局部搜索的思想,完备算法主要基于回溯搜索的思想。完备算法的优点在于一定能够判定SAT问题的可满足性。目前,最流行的完备算法是CDCL算法,本文则是基于CDCL算法结构展开研究,主要取得了如下研究成果:1.在EVSIDS和ACIDS算法的启发下,提出了一种基于动态奖励的分支启发式算法,也称为DRB算法。每当冲突发生时,DRB算法通过综合考虑变量决策层、冲突层、冲突次数和变量冲突频率进行活性分数更新,从而引导求解器的分支变量决策。2.根据学习子句的LBD值引入了层次差,用于评估LBD值相同的学习子句之间的质量差异。基于此,提出了基于层次差的学习子句删除启发式策略,也称为LDCR策略,从而指导求解器的子句数据库管理。3.将DRB算法和LDCR策略嵌入到Glucose 3.0与MapleLCMDistChronoBT求解器中,得到了6个新的SAT求解器。主要做了两类实验,实验一是基于Glucose 3.0的改进求解器与Glucose 3.0之间的对比实验,选择2015年、2016年和2017年三年的SAT竞赛实例进行测试;实验二是基于2018年冠军求解器MapleLCMDistChronoBT的改进求解器与MapleLCMDistChronoBT之间的对比实验,选择2018年的SAT竞赛实例进行测试。将改进求解器的测试结果与原来的求解器进行对比分析,实验结果表明改进求解器的性能均高于原来的求解器。因此,本文提出的两种新的启发式策略可以有效改进已有的CDCL算法框架,进而提升求解器的性能。

关键词： SAT问题 CDCL算法分支启发式策略学习子句删除启发式策略 DRB算法 LDCR策略 CDCL SAT求解器

来源：评论

学校读者我要写书评

暂无评论

SAT求解器中变量分支策略与学习子句管理策略研究

SAT求解器中变量分支策略与学习子句管理策略研究

引用

作者：孙菁西南交通大学

学位级别：硕士

知识表示和自动推理是人工智能领域的核心挑战,命题逻辑作为知识表示的一般方法,为定理证明提供了理论支撑,为计算机程序提供了验证、编译、可靠性分析。SAT求解器对提高命题逻辑问题可处理性做出了重要贡献,并在实际应用中取得显著成... 详细信息

知识表示和自动推理是人工智能领域的核心挑战,命题逻辑作为知识表示的一般方法,为定理证明提供了理论支撑,为计算机程序提供了验证、编译、可靠性分析。SAT求解器对提高命题逻辑问题可处理性做出了重要贡献,并在实际应用中取得显著成果。本文基于命题逻辑对SAT求解器中的相关策略展开研究,提出基于决策层的混合分支启发式策略和基于简化活性的学习子句集成管理策略,分别嵌入以CDCL(ConflictDriven Clause Learning)框架为核心的SAT求解器,具体成果如下:1、在变量的分支决策环节,变量赋值决策层和当前决策层被用于决策评估。一方面,对参与冲突分析的变量,提出了基于决策层的VSIDS＿dl(Variable State Independent Decaying Sum＿Decision Level)启发式策略;另一方面,对回溯过程中取消赋值的变量,根据强化学习,将回溯层次差作为学习率增量的一部分,提出了基于决策层的LRB＿dl(Learning Rate-based Branching＿Decision Level)启发式策略。并以分段式和交替式混合上述两种启发式策略,嵌入三个求解器中,形成对应的混合型分支启发式策略求解器,进行对比实验。结果表明,在求解图着色和平面色数问题时,基于决策层的交替式混合分支启发式策略在Maple COMSPS求解系统中显现出求解优势。2、在学习子句管理中,针对学习子句活跃值的计算复杂性和局限性,提出基于简化活性的学习子句评估标准。通过排序和标记的方法将其嵌入Maple LCMDist Chrono BT求解器中,实现了对全局学习子句参与冲突分析次数的简易评估和数据存储。实验结果表明:基于简化活性排序的集成管理策略能提高求解器的求解速率,基于简化活性标记的集成管理策略能解出部分原求解器无法求解的问题。

关键词：命题逻辑 SAT求解器分支启发式策略学习子句管理策略学习子句评估

来源：评论

学校读者我要写书评

暂无评论

一个高效、健壮的SAT程序的研究与开发

一个高效、健壮的SAT程序的研究与开发

引用

作者：焦加麟上海交通大学

学位级别：硕士

该文在探讨了SAT算法及其实现技术的基础上,描述了作者为了实现一个高效、健壮的SAT程序而进行的研究和实验工作,主要内容包括:第一,为了能够高效地实现SAT程序并能够在同等条件下比较各种不同的算法和技术,作者在总结前人成果和经验的... 详细信息

该文在探讨了SAT算法及其实现技术的基础上,描述了作者为了实现一个高效、健壮的SAT程序而进行的研究和实验工作,主要内容包括:第一,为了能够高效地实现SAT程序并能够在同等条件下比较各种不同的算法和技术,作者在总结前人成果和经验的基础上,结合自己的想法,设计了一个通用的基于DPLL的SAT程序框架:3D-DPLL框架.作者利用3D-DPLL框架来实现了自己的SAT程序,并且借助3D-DPLL作为测试台比较了几种分支决策策略和SAT算法;第二,作者实现了一个新的高效、健壮的SAT程序QuickSAT.在高效地集成了几种已经被证明了能有效提高SAT程序运行性能的算法策略.实验结果表明,在性能上,QuickSAT与当今世界上最高效的非商用完备类SAT程序zChaff相差无几,而在健壮性上比起几个当今最先进的SAT程序都要稍胜一筹,即QuickSAT能够在规定时间内解决更多的SAT问题.

关键词： SAT DPLL 分支启发式策略 BCP 智能回溯冲突分析

来源：评论

学校读者我要写书评

暂无评论

没有更多数据了...

全选清除本页清除全部题录导出标记到“检索档案”

共1页 << < 1 > >>

检索报告对象比较合并检索0

隐藏清空

合并搜索

回到顶部

执行限定条件

内容：

评分：

请选择保存的检索档案：

请选择收藏分类：

订阅名称：

通借通还

温馨提示：

图书名称：

借书校区：

取书校区：

手机号码：

邮箱地址：

一卡通帐号：

电话和邮箱必须正确填写，我们会与您联系确认。

联系人：

所在院系：

联系邮箱：

联系电话：

内蒙古自治区呼和浩特市赛罕区大学西街235号邮编: 010021

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：