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

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

张超;竺红卫;马琪

【期刊名称】《电路与系统学报》 【年(卷),期】2013(018)001

【摘要】Currently,Boolean satisfiability (SAT) solvers have been widely used in large circuit verification.Most SAT solvers are based on Davis-Putman-Logemann-Loveland (DPLL) algorithm and require the input formula to be in conjunctive normal formula (CNF).The CNF of a formula usually generates extra variables,and also destroys the structure information of the original circuit.In this paper,we propose several methods to solve this question.First,use AND/INVERTER graph transformation (AIG) to simplify the given circuits,and then,combine the graph characteristics of CNF and DNF,which will be used in Boolean Constraint Propagation (BCP) and speed up the BCP process.That is a key task in the DPLL algorithm.The efficiency of the proposed approach is shown through the experimental results on the ISCAS85 benchmark circuits.%现今,布尔可满足性(SAT)解算器己在工业电路验证过程中得到了广泛的应用.大多数SAT解算器是基于DPLL算法来构造的,需要电路输入形式是合取范式(CNF)的形式.CNF形式的构建会使电路表示正交化,但通常会产生更多的额外变量,同时也会破坏电路的原始结构信息,在使用DPLL算法搜索整个变量空间的时候需要大量的时间消耗.本文提出了一些方法来解决这些问题.首先使用与/非门(AIG)来简化待验证电路,然后在基于CNF的两变量观测策略上,结合合取

范式CNF和析取范式DNF的图特性来改善DPLL搜索过程,加速布尔约束推导(BCP)的进行.针对ISCAS85电路的验证结果验证了本算法的有效性. 【总页数】5页(42-46)

【关键词】布尔可满足性;与/非图;CNF;DNF;两变量观测策略;图特性 【作者】张超;竺红卫;马琪

【作者单位】浙江大学超大规模集成电路设计研究所,浙江杭州310027;浙江大学超大规模集成电路设计研究所,浙江杭州310027;浙江大学超大规模集成电路设计研究所,浙江杭州310027 【正文语种】中文 【中图分类】TN407 【文献来源】

https://www.zhangqiaokeyan.com/academic-journal-cn_journal-circuits-systems_thesis/0201234055311.html 【相关文献】

1.结合二叉判决图和布尔可满足性的等价性验证算法 [J], 严晓浪; 郑飞君; 葛海通; 杨军

2.两种加权观测融合算法的全局最优性和完全功能等价性 [J], 邓自立; 郝钢; 吴孝慧

3.求解Job-Shop约束满足问题的变量排序算法比较研究 [J], 尹静; 李铁克 4.值域增长约束满足问题的无回溯与随机行走策略的算法复杂性分析 [J], 徐伟; 巩馥洲

5.调查传播算法和蚁群算法相结合求解可满足性问题 [J], 王芙; 周育人; 叶立

以上内容为文献基本信息，获取文献全文请下载