Using AIG and Graph Characteristics in Boolean Satisfiability
Currently, Boolean satisfiability (SAT) solvers have been widely used in large circuit verification. Most SAT solvers are based on Davis-Putman-LogemannLoveland (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.
Boolean satisfiability AND/INVERTER graph CNF DNF two-watched-literal
Chao Zhang Hongwei Zhu
VLSI Institute Zhejiang University Hangzhou, Zhejiang Province, China
国际会议
重庆
英文
325-328
2011-08-20（万方平台首次上网日期，不代表论文的发表时间）