Abstract: In this paper, a new combinational equivalence checking approach using Boolean Satisfiability is proposed. The algorithm uses several methods to reduce the space of the SAT reasoning first, those methods are AND/INVERTER graph transformation, BDD propagation and implication learning, CNF-based SAT solver zChaff is used to solve the verification task. The algorithm combines the advantages of both BDD and SAT, BDDs size is limited to avoid memory explosion problem and structural reduction is applied to reduce the search space of SAT. The efficiency of the proposed approach is shown through its application on the ISCAS85 benchmark circuits.