OBDDs变量序的遗传算法求解策略

论文摘要

有序二叉判定图(OBDDs)是一种表示布尔函数的高效数据结构,在形式化验证领域内有着广泛应用。它为符号模型检测算法提供实现框架,使得模型检测中的状态空间爆炸问题得以缓解。OBDDs的规模严重地依赖于变量序,在最坏情况下其规模是呈指数级增长的。研究高效的变量排序算法,缩小其结点规模,对于提高符号模型检测效率具有至关重要的意义。OBDDs变量序问题已被证明是一个NP完全问题。现有的变量序求解算法,如:精确变量排序、启发式变量排序等,都是根据给定的函数结构对变量进行排序,对初始函数依赖性较强。因此具有一定的局限性,不能较好的解决这一问题。目前,遗传算法在求解该问题上效果较好。该算法以动态方式搜索最优解,摆脱了对给定函数的依赖性。但算法仍存在搜索效率低、局部优化能力弱、收敛速度慢等问题。为提升遗传算法求解OBDDs变量序问题的搜索效率,文章在原遗传算法基础上引入了自适应策略,并对其自适应模型进行改进。改进的算法根据种群进化程度动态调整交叉概率和变异概率,确保种群进化朝着正确方向进行,从而提升算法收敛速度和局部优化能力。算法通过调用软件包Buddy中部分内置函数测试样本获得实验数据。实验结果表明,改进的自适应遗传算法有效的降低了OBDDs规模,提高了算法的全局搜索能力。最高结点消减比例达14.67%,平均消减比例为2.58%。此外,针对两类特定类型布尔函数的OBDDs变量序,本文提出了特定的变量排序规则。并证明了在相应变量排序下布尔函数的OBDDs规模与其变量数是多项式相关的。

论文目录

• 摘要
• Abstract
• 1 绪论
•   1.1 研究背景及意义
•   1.2 研究现状
•   1.3 本文工作
•   1.4 文章结构
• 2 OBDDs变量序
•   2.1 有序二叉判定图
•     2.1.1 基本概念
•     2.1.2 BDDs构造
•   2.2 变量排序
•     2.2.1 OBDDs的变量序影响
•     2.2.2 静态变量排序法
•     2.2.3 动态变量排序法
•   2.3 两类布尔函数的OBDDs
•     2.3.1 变量排序规则
•     2.3.2 DNF布尔函数的OBDDs
•     2.3.3 CNF布尔函数的OBDDs
• 3 变量排序的遗传算法求解
•   3.1 遗传算法
•   3.2 基本流程
•     3.2.1 编码方式
•     3.2.2 适应度函数
•     3.2.3 遗传算子
•     3.2.4 参数设定
•   3.3 参数自适应
•     3.3.1 自适应模型
•     3.3.2 本文模型
• 4 算法实现与实验结果
•   4.1 算法实现
•     4.1.1 初始化与预处理
•     4.1.2 遗传算子
•     4.1.3 参数与终止条件
•     4.1.4 实验平台
•     4.1.5 实验数据
•   4.2 数据分析
•     4.2.1 算法收敛性
•     4.2.2 改善程度分析
• 结论
• 参考文献
• 硕士学位期间发表学术论文情况
• 致谢

文章来源

类型: 硕士论文

作者: 张媛

导师: 江建国

关键词: 有序二叉判定图,变量序,遗传算法,自适应,布尔函数

来源: 辽宁师范大学

年度: 2019

分类: 基础科学,信息科技

专业: 数学,自动化技术

单位: 辽宁师范大学

分类号: TP18;O157.5

总页数: 48

文件大小: 2518K

下载量: 13