论文部分内容阅读
电子设备的可靠性取决于其所采用的软硬件系统,归根到底,是其可靠的硬件基础——集成电路。集成电路的发展同时也促进计算机技术和通信技术的飞速发展,为此,保证集成电路拥有可靠的性能具有重要的现实意义。随着近年来可满足性问题(Boolean Satisfiability Problem,SAT)求解技术的研究发展,基于SAT求解器引擎的验证方法成为近年来集成电路验证领域一个新的研究热点。 DPLL(Davis-Putnam-Logemann-Loveland)算法是目前求解SAT问题最有效的算法,也是当前大部分SAT求解器的算法核心。尽管当前的SAT求解器已经集成了许多启发式搜索技术,但是仍然存在如下问题: 在DPL分支决策过程中,分支的选择仍然具有一定的盲目性,选择一个坏的分支进行决策推理很容易造成搜索树空间的增大,从而极大的影响算法的整体求解性能。 针对上述问题,本文在对DPLL算法开展深入研究后,提出了一个改进方案,主要完成的工作如下: 本文提出了一种带自适应噪声调整机制的混合SAT算法,并称之为ANHSAT。在ANHSAT中,将带有自适应噪声调整机制的局部搜索算法WalkSAT作为DPLL算法的前驱,将WalkSAT产生的近似解作为DPLL算法在分支决策时的优先参考子空间进行搜索。DPLL算法在选择变量准备分支推理时会优先分支近似解中的变量极性。实验结果表明,在与三种其他的SAT求解器比较中,提出的算法ANHSAT不仅在针对软硬件形式化验证领域的问题上表现出高效的性能,同时在其他实际问题(如人工智能规划、FPGA路由等)方面的求解上也表现出良好的性能。