无界模型检验中融合电路信息的SAT算法研究

A Novel Circuit SAT Solver in Unbounded Model Checking

针对从电路转化而来的SAT问题,通用SAT求解器存在一个缺陷——电路互连信息的缺失,这是造成很多无关推导的根源.文中提出了一个统一的基于CNF数据结构的电路SAT无界模型检验框架.首先作者提出了定值子句的概念,利用这一概念可以在CNF结构中保存电路的互连信息,在搜索过程中更早地识别可满足解,减少不必要的搜索.其次,文中提出了在CNF结构上的状态变量赋值精简方法,摆脱了以往基于SAT的无界模型检验中这一步骤对门级电路结构的依赖.实验数据表明,利用文中方法进行前像计算能够取得明显的加速.同时,文章比较了两种搜索顺序在多时帧搜索中的效果.实验结果表明利用文中方法可以验证传统模型检验方法难以验证的复杂电路属性.

For the circuit-oriented SAT problems, general purpose SAT solver will make some unnecessary decision and implication. The reason lies in that the circuit structure information is lost in the conversion to CNF. To overcome this drawback in SAT-based unbounded model checking, an improved SAT solver is proposed. First, the concept of define-value clauses is given to store the circuit structure in CNF. The improved solver avoids many redundant decisions which would be made by previous solvers. And then, A CNF-based assignment reduction algorithm is employed to speedup the convergence in search. The experimental result shows that the improved solver achieves obvious speedup over a previous method in preimage computation. The new method is capable of handling complex circuit property checking on which BDD-based methods would hardly work.