A Novel Method for All Solutions SAT Problem

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 donpsilat 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 donpsilat 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 is proposed. By experiment, it is proved to be very efficient for finding all solutions of SAT problems in EDA fields.