论文部分内容阅读
不良的ROBDD变量排序会引发状态空间爆炸的危机，从而影响形式验证方法的推广和使用。通过对CUDD数据包中ROBDD遗传变量排序算法的研究，利用变异操作和保留最优个体的时代繁殖操作对原算法进行了改进。实验数据表明，改进后的算法在可以容忍的运行时间内减少了ROBDD的节点数目，在一定程度上缓解了形式验证中状态空间爆炸的危机。