An Approach of Exploiting Observability Don't Cares in SAT Solver

To improve the efficiency of SAT solver,a new method using observability don't cares(ODC)is presented.Based on the theory of CNF carrying ODC condition,without ordering the variables in computing ODC conditions,the losses of ODC conditions are reduced.By making no decision on variables which only appear in the ODC conditions,the control uniqueness of the circuit is guaranteed.Theoretical analysis and experimental results show that the SAT solver implemented with this method has smaller search space and higher speed.