%0 Journal Article
%T 结合二叉判决图和布尔可满足性的等价性验证算法
%A 严晓浪
%A 郑飞君
%A 葛海通
%A 杨军
%J 电子学报
%P 1233-1235
%D 2004
%X 本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术.算法是在与/非图AIG中进行推理,并交替使用BDD扩展和基于电路SAT解算器简化电路.如尚未解决,将用基于合取范式SAT解算器进行推理.与已有算法相比主要有如下改进:在AIG中结合多种引擎进行简化,不存在误判可能;充分利用了基于电路解算器和基于合取范式解算器各自优点,减小了SAT推理的搜索空间.实验结果表明了本算法的有效性.
%K 等价性验证
%K 与/非图
%K 孤立节点
%K 二叉判决图
%K 可满足性解算器
%U http://www.ejournal.org.cn/CN/abstract/abstract2585.shtml