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