【摘要】 为了提高可满足性求解器的效率,提出了一种利用电路可观无关性的方法.以带可观无关条件的CNF理论为基础,通过在可观无关条件计算时不使用变量排序,减少可观无关条件丢失.通过不对只出现在可观无关条件中的变量赋值,保证电路的控制唯一性.理论分析和实验结果表明,用该方法实现的可满足性求解器的搜索空间小、速度快.更多还原

【Abstract】 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.更多还原