论文部分内容阅读
布尔可满足问题(SAT)作为第一个被证明的NP问题在许多方面有着重要的应用,该问题是人工智能、集成电路设计与验证、计算机科学、数理逻辑等领域中的核心问题,并且在计算机复杂性理论中有着十分重要的地位,作为NP问题,SAT问题无法在多项式时间内求解,因此高效的SAT求解器的设计一直被世界各国的学者所重视,SAT求解算法分为完备算法和不完备算法,求解器分为软件求解器和硬件求解器,其中硬件求解器又分为实例型求解器和应用型求解器。本文给出了两种基于FPGA的实例型硬件求解器的求解框架,即基于电路特征的求解框架和基于DPLL算法的求解框架,通过改变基于电路特征的求解框架中的激励模块实现了三种不同的求解方法,即顺序遍历激励求解、真随机数激励求解和伪随机数激励求解,并对三种求解方法的实验结果进行了对比和分析。对于基于DPLL算法的求解器,本文创新地在求解电路生成前对变量选取顺序和变量赋值顺序进行了随机排序,并对同一实例生成多个求解电路进行多次求解,对不同次数的求解结果进行了分析,并将所有实例的求解结果与其他硬件求解器及软件求解器Minisat进行了分析和对比。