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

作者：张一凡吉林大学

学位级别：硕士

作为布尔可满足性问题的重要拓展,模型计数是从人工智能到形式化验证的一项重要推理任务,其在概率推理、神经网络验证、自动规划等领域有着广泛的应用。可满足性问题是对于一个给定的命题逻辑公式φ,判断是否存在满足该公式的赋值,而模... 详细信息

作为布尔可满足性问题的重要拓展,模型计数是从人工智能到形式化验证的一项重要推理任务,其在概率推理、神经网络验证、自动规划等领域有着广泛的应用。可满足性问题是对于一个给定的命题逻辑公式φ,判断是否存在满足该公式的赋值,而模型计数问题是计算满足公式φ的赋值的数量,计算复杂度是#P完全,故模型计数问题相较于可满足性问题更具有挑战性。随着学界对模型计数相关算法研究的不断深入以及模型计数应用需求的持续增长,再加之模型计数竞赛的推广,社区中已经出现了数十种模型计数求解器,这些求解器使用的求解算法主要分为三类:基于搜索、基于编译以及基于变量消除。基于搜索的模型计数方法通过更智能的枚举部分解去扩展DPLL框架;基于编译的技术依赖于高效的知识编译器,编译器将输入语言表示的公式编译为目标语言,编译完成后基于目标语言的表示高效地进行模型计数;基于变量消除的方法主要通过对变量进行一系列求和来执行模型计数。随着模型计数求解器的广泛应用,人们逐渐发现不存在单一求解器在大规模实例集的所有实例上表现都比其他求解器好,即没有单一的主导性求解器。相反,不同求解器在不同实例上表现各不相同,主要原因是不同实例有着不同的特征,而使用不同求解算法的求解器在具有不同特征的实例上会表现出较大差异。如果能根据实例的特征使用机器学习分类器为不同的实例选择不同的求解器,那么将有效地增加求解实例的数量并大幅度降低求解时间。基于这个问题,本文设计并实现了基于求解器选择的模型计数求解器SmartMC,其主要思想是计算实例的特征并使用机器学习分类器根据特征进行求解器选择。SmartMC使用的特征基于9类常用的表现命题逻辑公式特性的特征并在此基础上进行了特征选择,此外本文还加入了与模型计数任务相关的特征。本文还对神经网络求解器进行了研究与探索,提出并实现了基于信念传播的神经网络模型计数求解器BPMC,其能在极短的时间内给出实例的近似模型计数值,并且求解时间基本不受实例规模的影响。本文将SmartMC与神经网络求解器BPMC进行了结合,即当SmartMC无法求解实例时,使用神经网络求解器BPMC在极短时间内获得近似模型计数值,保证SmartMC对于任意实例一定能给出结果,进一步提升SmartMC的完备性。本文设计了两组实验,第一个组实验将神经网络求解器BPMC与目前先进的近似模型计数求解器Approx MC、信念传播神经网络BPNN进行对比,实验结果表明BPMC的准确度接近Approx MC,优于BPNN,但是在求解时间上,BPMC花费的求解时间远少于Approx MC,并且BPMC求解时间几乎不受实例规模的影响。第二组实验将关闭了神经网络求解器BPMC的SmartMC与目前先进的模型计数求解器sharp SAT-TD、Exact MC、Ganak、DPMC进行对比,实验结果表明,在求解实例的数量以及平均求解时间上,SmartMC的表现都优于目前先进的模型计数求解器。

关键词：模型计数机器学习求解器选择神经网络求解器

来源：评论

学校读者我要写书评

暂无评论

基于扩展规则的模型计数方法研究

基于扩展规则的模型计数方法研究

引用

作者：贾凤雨吉林大学

学位级别：硕士

早在二十世纪五十年代,智能规划一经提出便成为了人工智能领域中的一个前沿研究领域,自此,随着国内外诸多研究学者们不懈努力,在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法,其中一种较为高效的求解方法... 详细信息

早在二十世纪五十年代,智能规划一经提出便成为了人工智能领域中的一个前沿研究领域,自此,随着国内外诸多研究学者们不懈努力,在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法,其中一种较为高效的求解方法则是将规划问题编译为命题可满足性问题(SAT问题),然后利用SAT求解器进行求解。有时此种间接求解的方法会比直接求解的方法更为高效快捷,目前已成为求解智能规划问题的主流方法之一。在1971年,Cook等人证明SAT问题是NP完全的。事实上,许多NP问题都可以转为SAT问题进行求解。然而,在人工智能研究领域还有许多经典问题的计算复杂度是高于NP的,对于这些问题的求解仅仅判断给定命题公式是否可满足是不够的,还需要知道问题模型的个数。由此扩展出了模型计数问题(#SAT问题)。如贝叶斯网络推理,概率规划问题等都可以转化成#SAT问题进行求解。因此,如何高效地求解#SAT问题,对人工智能的很多领域都有重要意义。目前,求解#SAT问题的算法可以分为精确求解和近似求解两种。精确算法可以保证计算出给定命题公式的准确模型个数;而近似算法只能计算出给定公式模型的近似个数。在精确求解的算法中主要有基于DPLL(Davis Putnam Logemann and Loveland)的方法和基于扩展规则的方法。这两种方法是互补的求解方法。一般情况下,当互补因子较高时,基于扩展规则的求解方法要优于基于DPLL求解方法;反之,当互补因子较低时,要差于基于DPLL求解方法。本文在对基于扩展规则的模型计数求解方法CER深入研究的基础上,从不同角度对其进行改进,提出了两种更为高效的求解方法:(1)结合扩展规则重构的#SAT问题增量求解方法:对CER中的重要计算公式进行重构,并证明了重构的正确性;给出了极大项相交集和扩展极大项相交集的定义,并提出结合两者关系复用极大项相交集求解结果的增量计算方法,还删减了所有广义互补子句集对应的扩展极大项相交集,有效避免了许多冗余计算;给出用互补表记录子句间互补关系的方法,提出一种对极大项相交集的基础子句集进行增量判定互补的方法,很好地避免了在判定子句间及基础子句集互补性时的大量冗余计算。实验结果表明:与CER方法相比,RCER方法效率更高,尤其是互补因子较低的情况下。(2)结合互补度的基于扩展规则#SAT问题求解方法:在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合。并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备。提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数。实验结果表明,与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足。以上两种方法从不同角度对CER方法进行了改进,并取得了较好的效果。两种方法分别利用了CER方法中重要公式的计算项间的关系和计算顺序减少了求解过程中的冗余计算,从而达到提高效率的目的。

关键词：智能规划命题可满足性问题模型计数扩展规则增量方法

来源：评论

学校读者我要写书评

暂无评论

六种常见的“球”模型计数分析与相关概率

引用

高考(文科版) 2008年第Z2期 8-9页

作者：刘景鹏河北省广平县第一中学

来源：评论

学校读者我要写书评

暂无评论

最坏情况下#3-SAT问题最小上界

引用

计算机研究与发展 2011年第11期48卷 2055-2063页

作者：周俊萍殷明浩周春光翟延冬王康平吉林大学计算机科学与技术学院长春130012 东北师范大学计算机科学与信息技术学院长春130117 教育部符号计算与知识工程重点实验室(吉林大学) 长春130012

最坏情况下#SAT问题上界的研究已成为一个热门的研究领域.#SAT问题的时间复杂性是根据问题实例的大小所组成的函数计算所得.#SAT问题实例的大小不仅依赖于变量的数量,还依赖于子句的数量.以子句数量为参数研究#SAT问题在最坏情况下的上... 详细信息

最坏情况下#SAT问题上界的研究已成为一个热门的研究领域.#SAT问题的时间复杂性是根据问题实例的大小所组成的函数计算所得.#SAT问题实例的大小不仅依赖于变量的数量,还依赖于子句的数量.以子句数量为参数研究#SAT问题在最坏情况下的上界,不仅可以从另一个角度衡量算法的好坏,而且在某种程度上更能准确地反映出算法的性能.首先从子句数量的角度证明了之前提出的基于扩展规则的模型计数算法(CER算法)的上界O(2m),其中m是公式中子句的数量.为了提高#3-SAT问题的求解效率,采用了多种分裂规则,进一步给出了一种基于Davis-Putnam-Logemann-Loveland(DPLL)的#3-SAT算法MCDP.通过分析该算法得到了以子句数量为参数的#3-SAT问题在最坏情况下的上界O(1.8393m).

关键词：最坏情况上界 #3 SAT 复杂性分析模型计数

来源：评论

学校读者我要写书评

暂无评论

基于扩展规则的启发式#SAT求解算法

引用

软件学报 2018年第11期29卷 3517-3527页

作者：王强刘磊吕帅吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 吉林长春130012

#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究,发现选择规约子句的顺序对极大项空间的大小有着较大的影响,因此提出两种加速#SAT求解的启... 详细信息

#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究,发现选择规约子句的顺序对极大项空间的大小有着较大的影响,因此提出两种加速#SAT求解的启发式策略:MW和LC&***每次选择具有最大权值的子句作为规约子句;LC&MW每次选择最长子句作为规约子句,若最长子句存在多个,则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CER_MW,利用LC&MW策略设计了算法CER_LC&MW.实验结果表明,CER_MW和CER_LC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面,CER_MW和CER_LC&MW的求解速度是其他算法的1.4倍~100倍.在求解能力方面,CER_MW和CER_LC&MW在限定时间内可解的测试用例更多.

关键词：扩展规则模型计数启发式算法极大项空间规约子句

来源：评论

学校读者我要写书评

暂无评论

两种新的基于扩展规则#SAT问题求解算法

引用

东北大学学报（自然科学版） 2019年第5期40卷 630-634,646页

作者：吕帅张桐搏王强刘磊吉林大学计算机科学与技术学院吉林长春130012

提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样... 详细信息

提出一种新的基于扩展规则的#SAT求解算法NCER,该算法在#ER的基础上加入启发式策略.该策略每次选择当前子句集的最长子句来减小极大项空间,使得递归调用的次数减少,从而加快求解效率.为解决基于扩展规则的#SAT求解器在互补因子较小的样例上的不良表现,结合NCER和CDP的优点提出混合#SAT求解算法NCDPER.实验结果表明:NCER较先前的#ER在所有85个随机SAT测试用例上有了显著的提高.通过与目前最好的基于扩展规则的#SAT求解器的比较,该求解器具有更好的性能.

关键词：自动推理扩展规则模型计数极大项空间启发式策略

来源：评论

学校读者我要写书评

暂无评论

一种基于扩展规则的#SAT求解系统

引用

软件学报 2009年第7期20卷 1714-1725页

作者：殷明浩林海孙吉贵吉林大学计算机科学与技术学院吉林长春130012 吉林大学符号计算与知识工程教育部重点实验室吉林长春130012 东北师范大学计算机学院吉林长春130117

#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有... 详细信息

#SAT问题是SAT问题的扩展,需要计算出给定命题公式集合的模型个数.通过将问题求解沿着归结的反方向进行,并利用容斥原理解决由此带来的空间复杂性问题,提出了一种基于扩展规则的模型计数和加权模型计数问题求解框架,可以看作是目前所有模型计数问题求解方法的一种补方法.证明了该方法的完备性和有效性,设计了基于扩展规则的#SAT求解系统:JLU-ERWMC.实验结果表明,JLU-ERWMC在有些问题中优于目前最为高效的#SAT问题求解系统.

关键词：扩展规则模型计数知识编译加权模型计数

来源：评论

学校读者我要写书评

暂无评论

工作流可满足性的约简增量模式回溯法

引用

计算机集成制造系统 2023年第11期29卷 3624-3638页

作者：翟治年刘关俊卢亚辉向坚吴茗蔚丰明坤浙江科技学院信息与电子工程学院浙江杭州310023 同济大学计算机科学系上海201804 深圳大学计算机与软件学院广东深圳518060

在大量云/服务化资源造成的性能压力下,增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径,但对“欠约束”实例,其模式枚举性能显著下降,不利于大量可行解的优化选择。针对该问题提... 详细信息

在大量云/服务化资源造成的性能压力下,增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径,但对“欠约束”实例,其模式枚举性能显著下降,不利于大量可行解的优化选择。针对该问题提出新颖的简指派图概念,证明其可取代k指派图用于模式授权匹配验证,且尽管其块邻域大小耦合了图的整体信息,但仍可以增量方式计算。进而,分析了增量化简指派的实施条件和效果,及其主要影响因素。由此建立了约简增量模式回溯法(Reduced Incremental Pattern Backtracking, RIPB)。在资源配比为2~100的两个仿真实例集上测试,实验结果表明:在其基本子集上,RIPB较IPB有0.96~1.24倍时间性能优势;当资源比例升高或约束密度降低时,RIPB的优势有不同程度扩大;特别地,对资源配比为10而授权比例在1/2左右的两个子集,RIPB的平均优势分别可达1.29和1.61倍。

关键词：可满足性工作流授权约束资源分配模型计数模式

来源：评论

学校读者我要写书评

暂无评论

结合扩展规则重构的#SAT问题增量求解方法

引用

软件学报 2015年第12期26卷 3117-3129页

作者：贾凤雨欧阳丹彤张立明刘思光吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 吉林长春130012

#SAT问题是人工智能中的重要问题,在人工智能领域被广泛应用.在对基于扩展规则的模型计数求解方法CER深入研究的基础上,重构CER中使用的计算公式,并对其正确性进行了证明;提出极大项相交集和扩展极大项相交集的概念,并给出根据两者关系... 详细信息

#SAT问题是人工智能中的重要问题,在人工智能领域被广泛应用.在对基于扩展规则的模型计数求解方法CER深入研究的基础上,重构CER中使用的计算公式,并对其正确性进行了证明;提出极大项相交集和扩展极大项相交集的概念,并给出根据两者关系重用极大项相交集计算结果的增量求解方法,且对广义互补子句集对应的所有扩展极大项相交集进行剪枝,有效避免了计算所有极大项相交集对应极大项个数时的冗余求解;提出构建记录子句间互补关系的互补表方法,给出重用极大项相交集基础子句集互补结果的增量互补判定方法,较好地避免了判断子句间和各极大项相交集的基础子句集互补关系时的重复计算.实验结果表明:RCER方法易于实现,扩展性强,比CER方法效率更高,尤其是在互补因子较低时,效率提升更为显著.

关键词：扩展规则模型计数极大项相交集互补表增量方法

来源：评论

学校读者我要写书评

暂无评论

结合互补度的基于扩展规则#SAT问题求解方法

引用

计算机研究与发展 2016年第7期53卷 1596-1604页

作者：欧阳丹彤贾凤雨刘思光张立明吉林大学计算机科学与技术学院长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 长春130012

#SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一,在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法 CER(counting models using extension rules)深入研究的基础上,提出一种结合互补度的#SAT问题... 详细信息

#SAT问题又称模型计数(model counting)问题是人工智能领域的研究热点之一,在人工智能领域被广泛应用.在对基于扩展规则的#SAT问题求解方法 CER(counting models using extension rules)深入研究的基础上,提出一种结合互补度的#SAT问题求解方法.在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合,并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备.提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数.实验结果表明:与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足.

关键词：扩展规则模型计数 CER方法互补度集合枚举树

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：