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