结合AIG和两变量观测策略的SAT满足性算法

• 作者: 张超 竺红卫 马琪
• 来源期刊: 新能源进展
• 学科: 工学
• 关键词: 布尔可满足性 与/非图 CNF DNF 两变量观测策略 图特性
• 年，卷（期）: 2013,（1）
• 所属期刊栏目: 论文
• 页码范围: 42-46
• 页数: 5页
• 分类号: TN407
• 字数: 3234字
• 语种: 中文

摘要

现今,布尔可满足性(SAT)解算器己在工业电路验证过程中得到了广泛的应用.大多数SAT解算器是基于DPLL算法来构造的,需要电路输入形式是合取范式(CNF)的形式.CNF形式的构建会使电路表示正交化,但通常会产生更多的额外变量,同时也会破坏电路的原始结构信息,在使用DPLL算法搜索整个变量空间的时候需要大量的时间消耗.本文提出了一些方法来解决这些问题.首先使用与/非门(AIG)来简化待验证电路,然后在基于CNF的两变量观测策略上,结合合取范式CNF和析取范式DNF的图特性来改善DPLL搜索过程,加速布尔约束推导(BCP)的进行.针对ISCAS85电路的验证结果验证了本算法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张超	浙江大学超大规模集成电路设计研究所	62	962	14.0	30.0
2	马琪	浙江大学超大规模集成电路设计研究所	6	18	2.0	4.0
3	竺红卫	浙江大学超大规模集成电路设计研究所	20	83	5.0	7.0