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

Combining AIG and advanced two-watched-literal in SAT boolean

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

Currently,Boolean satisfiability（SAT） solvers have been widely used in large circuit verification.Most SAT solvers are based on Davis-Putman-Logemann-Loveland（DPLL） algorithm and require the input formula to be in conjunctive normal formula（CNF）.The CNF of a formula usually generates extra variables,and also destroys the structure information of the original circuit.In this paper,we propose several methods to solve this question.First,use AND/INVERTER graph transformation（AIG） to simplify the given circuits,and then,combine the graph characteristics of CNF and DNF,which will be used in Boolean Constraint Propagation（BCP） and speed up the BCP process.That is a key task in the DPLL algorithm.The efficiency of the proposed approach is shown through the experimental results on the ISCAS85 benchmark circuits.