二叉判定图(BDD)是描述布尔函数或组合逻辑电路的一种数据结构，广泛应用于形式验证领域，包括组合逻辑电路、时序逻辑电路，以及等价性检验、模型检验等，被许多用于电路设计的CAD系统作为底层数据结构。不过，在实际应用中，能否使用二叉判定图进行求解，很大程度上取决于使用BDD表示问题时所需的存储空间大小，即，BDD的节点规模，而这是严重依赖于变量序列的。对BDD变量排序相关的研究，能够大幅降低BDD节点规模，进而缓解模型检验态空间爆炸问题，具有十分重要的意义。文章简要介绍了BDD相关基础理论和变量排序相关情况，并在传统遗传算法的BDD变量排序算法基础上，基于灾变的概念，提出了灾变自适应遗传算法，用以求解BDD变量最小化问题。该算法能够根据需要动态调整算法交叉和变异概率，降低对初始参数的依赖，减少算法运行负担，并能在不扩大种群规模的情况下，极大地增加了个体多样性，改善遗传算法的早熟收敛问题。而且，由于算法本身并不关心发生灾变之前种群的进化方式与进化方向，因而极易与其它改进策略结合起来，特别是一些局部搜索效率较高的算法，能够在原有特性的基础上引入全局优势，进一步减小节点规模，扩展余地十分充足。论文使用Uniform Random-3-SAT测试集的基准样本进行测试。试验结果表明：灾变算法的全局特性显著优于传统遗传算法，能够在基本遗传算法的基础上进一步减小节点规模，平均改善程度约为11%，最高改善程度可达25%。而引入自适应策略以后，平均改善程度得以进一步提高，达到12.82%，最高改善程度可达26.9%。