结合AIG和两变量观测策略的SAT满足性算法
Combining AIG and advanced two-watched-literal in SAT boolean
张超 1竺红卫 1马琪1
作者信息
- 1. 浙江大学超大规模集成电路设计研究所,浙江杭州310027
- 折叠
摘要
现今,布尔可满足性(SAT)解算器己在工业电路验证过程中得到了广泛的应用.大多数SAT解算器是基于DPLL算法来构造的,需要电路输入形式是合取范式(CNF)的形式.CNF形式的构建会使电路表示正交化,但通常会产生更多的额外变量,同时也会破坏电路的原始结构信息,在使用DPLL算法搜索整个变量空间的时候需要大量的时间消耗.本文提出了一些方法来解决这些问题.首先使用与/非门(AIG)来简化待验证电路,然后在基于CNF的两变量观测策略上,结合合取范式CNF和析取范式DNF的图特性来改善DPLL搜索过程,加速布尔约束推导(BCP)的进行.针对ISCAS85电路的验证结果验证了本算法的有效性.
Abstract
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.
关键词
布尔可满足性/与/非图/CNF/DNF/两变量观测策略/图特性Key words
boolean satisfiability/AND/INVERTER graph/CNF/DNF/two-watched-literal/graph characteristi(c)s引用本文复制引用
出版年
2013
NETL
NSTL
维普
万方数据