All-solution Boolean satisfiability (SAT) solver has been widely used throughout the EDA industry fields, such as formal verification, circuit synthesis and automatic test pattern generation. Exploiting structure information especially Observability Don’t Cares(ODCs) of circuits can improve the efficiency of SAT solvers. The authors converted the ODC property of signal to clauses of CNF formula by adding don’t care literals conditions to clauses in the CNF formula. This can reduce the problem scale during the process of variable assigned greatly. In this paper, this new method is used to the all solutions SAT problem and a new all solutions SAT solver isproposed. By experiment, it is proved to be very efficient for finding all solutions of SAT problems in EDA fields.