|
|||||
|
|
| 基于OBDD的SMC中PRE 操作的改进算法 | |
| 引用本文： | 姚全珠,魏小勇.基于OBDD的SMC中PRE 操作的改进算法[J].计算机工程,2008,34(14). |
| 作者姓名： | 姚全珠 魏小勇 |
| 作者单位： | 西安理工大学计算机科学与工程学院,西安710048 |
| 摘 要： | 提出一种基于排序二值判定图（OBDD）的符号模型检测中PRE 操作的改进算法。该算法处理PRE 步骤3（嵌套布尔存在量化）的方法是一次遍历“删除”所有被量化变量的节点,产生表示布尔函数与嵌套存在量化结果等价的不确定排序二值判定图,把不确定排序二值判定图转换成OBDD。实验表明,该算法能有效缩短计算时间,减少中间节点所需空间。 |
| 关 键 词： | 排序二值判定图 符号模型检测 PRE 操作 深度优先搜索 |
| 本文献已被 维普 等数据库收录！ | |