结合AIG和两变量观测策略的SAT满足性算法

现今,布尔可满足性(SAT)解算器已在工业电路验证过程中得到了广泛的应用。大多数SAT解算器是基于DPLL算法来构造的,需要电路输入形式是合取范式(CNF)的形式。CNF形式的构建会使电路表示正交化,但通常会产生更多的额外变量,同时也会破坏电路的原始结构信息,在使用DPLL算法搜索整个变量空间的时候需要大量的时间消耗。本文提出了一些方法来解决这些问题。首先使用与/非门(AIG)来简化待验证电路,然后在基于CNF的两变量观测策略上,结合合取范式CNF和析取范式DNF的图特性来改善DPLL搜索过程,加速布尔约束推导(BCP)的进行。针对ISCAS85电路的验证结果验证了本算法的有效性。