基于图及树结构的极小不可满足集求解方法
发布时间：2022-01-12 15:16
命题可满足问题（propositional satisfiability problem,SAT）是人工智能领域的研究热点,也是数理逻辑及计算机研究中的核心问题,对人工智能发展起到了非常重要的推动作用。命题可满足问题擅长将一些艰难的故障求解转化为问题系统中命题公式是否存在可满足赋值的问题,并给出故障识别。极小不可满足集（minimal unsatisfiable subset,MUS）问题是命题可满足问题的扩展问题。在求解极小不可满足解时,通常将不可满足性问题转换为命题可满足问题,利用SAT求解器来给出是否一致可满足的判定。目前求解极小不可满足集效率较高的两种遍历结构为哈斯图和枚举树。哈斯图结构主要是利用图的逻辑结构构建节点之间的联系,适用于广泛的约束关系处理。图结构主要应用于关系规范调试、不一致检测、模型验证等问题中。极小冲突问题是极小不可满足问题在基于模型诊断上的应用,主要采用枚举树结构,利用树的特性对电路系统中元件集的全枚举进行遍历。相对于图结构遍历,树结构遍历求解极小冲突问题节点跳转方便,配合剪枝策略剪去枚举树中不需要遍历的节点使求解效率更快。在基于图结构求解方法中,MARCO...
【文章来源】：吉林大学吉林省 211工程院校 985工程院校 教育部直属院校
【文章页数】：55 页
【学位级别】：硕士
【文章目录】：
摘要
abstract
第1章 绪论
1.1 研究背景和意义
1.2 研究现状
1.3 本文工作
第2章 极小不可满足问题
2.1 SAT相关概念
2.2 极小不可满足集
2.3 遍历结构
2.3.1 图结构求解极小不可满足问题
2.3.2 树结构求解极小冲突集问题
2.4 本章小结
第3章 基于双模型的MUS求解方法
3.1 相关定义
3.2 基于极大化模型的MARCO方法
3.3 基于双模型的MARCO-MAM方法
3.4 实例对比分析
3.5 实验结果及分析
3.6 本章小结
第4章 结合故障逻辑关系的极小冲突集求解方法
4.1 相关定义
4.2 结合故障输出的MCS-SFFO方法
4.3 结合故障输出逻辑结构的MCS-FLR方法
4.4 MCS-FLR算法分析
4.5 实例对比分析
4.6 实验结果与分析
4.7 本章小结
第5章 总结与展望
5.1 工作总结
5.2 工作展望
参考文献
作者简介及在学期间所取得的科研成果
致谢
【参考文献】：
期刊论文
[1]基于子集一致性检测的诊断解极小性判定方法[J]. 田乃予,欧阳丹彤,刘梦,张立明. 计算机研究与发展. 2019(07)
[2]结合故障输出结构特征的极小冲突求解算法[J]. 徐旖旎,欧阳丹彤,刘梦,张立明,张永刚. 计算机研究与发展. 2018(11)
[3]Efficient zonal diagnosis with maximum satisfiability[J]. Meng LIU,Dantong OUYANG,Shaowei CAI,Liming ZHANG. Science China（Information Sciences）. 2018(11)
[4]结合问题特征的分组式诊断方法[J]. 刘梦,欧阳丹彤,刘伯文,张立明,张永刚. 电子学报. 2018(03)
[5]结合问题特征利用SE-Tree反向深度求解冲突集的方法[J]. 欧阳丹彤,刘伯文,周建华,张立明. 电子学报. 2017(05)
[6]基于模型诊断中结合问题特征的新方法[J]. 欧阳丹彤,周建华,刘伯文,张立明. 计算机研究与发展. 2017(03)
[7]结合SE-Tree结构特征的极小碰集求解算法[J]. 刘思光,欧阳丹彤,王艺源,贾凤雨,张立明. 计算机研究与发展. 2016(11)
[8]使用SAT求解器产生所有极小冲突部件集[J]. 赵相福,欧阳丹彤. 电子学报. 2009(04)
[9]一种基于ATMS的求解所有极小冲突集的新方法[J]. 张立明,欧阳丹彤,赵相福. 计算机工程与科学. 2007(11)
[10]A method of combining SE-tree to compute all minimal hitting sets[J]. ZHAO Xiangfu and OUYANG Dantong (School of Computer Science and Technology, Jilin University, Changchun 130012, China; Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Changchun 130012, China). Progress in Natural Science. 2006(02)
本文编号：3585001
【文章来源】：吉林大学吉林省 211工程院校 985工程院校 教育部直属院校
【文章页数】：55 页
【学位级别】：硕士
【文章目录】：
摘要
abstract
第1章 绪论
1.1 研究背景和意义
1.2 研究现状
1.3 本文工作
第2章 极小不可满足问题
2.1 SAT相关概念
2.2 极小不可满足集
2.3 遍历结构
2.3.1 图结构求解极小不可满足问题
2.3.2 树结构求解极小冲突集问题
2.4 本章小结
第3章 基于双模型的MUS求解方法
3.1 相关定义
3.2 基于极大化模型的MARCO方法
3.3 基于双模型的MARCO-MAM方法
3.4 实例对比分析
3.5 实验结果及分析
3.6 本章小结
第4章 结合故障逻辑关系的极小冲突集求解方法
4.1 相关定义
4.2 结合故障输出的MCS-SFFO方法
4.3 结合故障输出逻辑结构的MCS-FLR方法
4.4 MCS-FLR算法分析
4.5 实例对比分析
4.6 实验结果与分析
4.7 本章小结
第5章 总结与展望
5.1 工作总结
5.2 工作展望
参考文献
作者简介及在学期间所取得的科研成果
致谢
【参考文献】：
期刊论文
[1]基于子集一致性检测的诊断解极小性判定方法[J]. 田乃予,欧阳丹彤,刘梦,张立明. 计算机研究与发展. 2019(07)
[2]结合故障输出结构特征的极小冲突求解算法[J]. 徐旖旎,欧阳丹彤,刘梦,张立明,张永刚. 计算机研究与发展. 2018(11)
[3]Efficient zonal diagnosis with maximum satisfiability[J]. Meng LIU,Dantong OUYANG,Shaowei CAI,Liming ZHANG. Science China（Information Sciences）. 2018(11)
[4]结合问题特征的分组式诊断方法[J]. 刘梦,欧阳丹彤,刘伯文,张立明,张永刚. 电子学报. 2018(03)
[5]结合问题特征利用SE-Tree反向深度求解冲突集的方法[J]. 欧阳丹彤,刘伯文,周建华,张立明. 电子学报. 2017(05)
[6]基于模型诊断中结合问题特征的新方法[J]. 欧阳丹彤,周建华,刘伯文,张立明. 计算机研究与发展. 2017(03)
[7]结合SE-Tree结构特征的极小碰集求解算法[J]. 刘思光,欧阳丹彤,王艺源,贾凤雨,张立明. 计算机研究与发展. 2016(11)
[8]使用SAT求解器产生所有极小冲突部件集[J]. 赵相福,欧阳丹彤. 电子学报. 2009(04)
[9]一种基于ATMS的求解所有极小冲突集的新方法[J]. 张立明,欧阳丹彤,赵相福. 计算机工程与科学. 2007(11)
[10]A method of combining SE-tree to compute all minimal hitting sets[J]. ZHAO Xiangfu and OUYANG Dantong (School of Computer Science and Technology, Jilin University, Changchun 130012, China; Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Changchun 130012, China). Progress in Natural Science. 2006(02)
本文编号：3585001
本文链接：https://www.wllwen.com/shoufeilunwen/benkebiyelunwen/3585001.html
