形式验证中ROBDD变量排序算法的研究

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

Research on ROBDD Variables Reordering Algorithm in Formal Verification

The ill order of ROBDD variables may cause the crisis of state space explosion and,therefore,influence the use of the formal verification method.In this paper,we present an improved algoribhm by adding mutation and optimized evolution operations to the genetic ROBDD variables reordering algorithm in the CUDD package.The experimental results demonstrate that the proposed algorithm can reduce the number of ROBDD nodes within a tolerable time,and slow down the crisis of state space explosion in the formal veri...