Heuristic Boolean satisfiability algorithm based on grouping
Zhang Bi-ying · Computer Engineering and Applications Journal · 2008
The paper gives the study of binary decision diagrams and Boolean satisfiability algorithms in formal verification method.It improves on Boolean satisfiability algorithms,and gives the DCDS algorithms.The paper gives equivalence checking algorithms in combinational circuit based on SAT,the arithmetic integrates the strongpoint of BDD and SAT,by restricting the size of constructing BDD,avoids EMS memory exploding.Reasoning minishes searching space of SAT.And apply this new algorithm in formal verification method based on BDD-SAT.Theoretical research and experimence results have proved the correctness of algorithms and design methods proposed in this paper.