基于FPGA的实例型SAT求解芯片的设计与实现

发布时间：2018-05-20 04:48

本文选题：布尔可满足 + 现场可编程门阵列　；参考：《广西民族大学》2017年硕士论文

【摘要】：布尔可满足问题(SAT)作为第一个被证明的NP问题在许多方面有着重要的应用,该问题是人工智能、集成电路设计与验证、计算机科学、数理逻辑等领域中的核心问题,并且在计算机复杂性理论中有着十分重要的地位,作为NP问题,SAT问题无法在多项式时间内求解,因此高效的SAT求解器的设计一直被世界各国的学者所重视,SAT求解算法分为完备算法和不完备算法,求解器分为软件求解器和硬件求解器,其中硬件求解器又分为实例型求解器和应用型求解器。本文给出了两种基于FPGA的实例型硬件求解器的求解框架,即基于电路特征的求解框架和基于DPLL算法的求解框架,通过改变基于电路特征的求解框架中的激励模块实现了三种不同的求解方法,即顺序遍历激励求解、真随机数激励求解和伪随机数激励求解,并对三种求解方法的实验结果进行了对比和分析。对于基于DPLL算法的求解器,本文创新地在求解电路生成前对变量选取顺序和变量赋值顺序进行了随机排序,并对同一实例生成多个求解电路进行多次求解,对不同次数的求解结果进行了分析,并将所有实例的求解结果与其他硬件求解器及软件求解器Minisat进行了分析和对比。
[Abstract]:As the first proven NP problem, Boolean satisfiability problem has important applications in many fields. It is the core problem in the fields of artificial intelligence, integrated circuit design and verification, computer science, mathematical logic, etc. And it plays an important role in the theory of computer complexity. As a NP problem, the SAT problem can not be solved in polynomial time. Therefore, the design of efficient SAT solver has been paid much attention by scholars all over the world. The algorithm is divided into complete algorithm and incomplete algorithm, and solver is divided into software solver and hardware solver. The hardware solver is divided into example solver and application solver. In this paper, two kinds of hardware solver based on FPGA are presented, which are based on circuit characteristics and DPLL algorithm. By changing the excitation module of the circuit characteristic based solution framework, three different solutions are realized, namely, sequential traversal excitation solution, true random number excitation solution and pseudo random number excitation solution. The experimental results of the three methods are compared and analyzed. For the solver based on DPLL algorithm, this paper innovatively sorts the variable selection order and the variable assignment order before the generation of the solving circuit. The solution results of different times are analyzed and compared with other hardware solver and software solver Minisat.
【学位授予单位】：广西民族大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TN402

【参考文献】