Study On Framework And System Of Solving The SAT Problems On The ZYNQ Platform

Boolean Satisfiability(SAT)problem is one of the key and basic problems in the fields of mathematical logic and computer theory,and it is also the first problem that was proven to be NP-Complete.Theoretically,many problems can be reduced into SAT problem in a polynomial time.Therefore,many practical problems can be solved by the solutions of SAT problem.At present,the SAT problem has been widely used in the fields of electronic design automation(EDA),artificial intelligence,mathematics,and biological information.Therefore,the method and framework for solving the SAT problem has always been a research point in related fields.First of all,this thesis studies the software and hardware solutions of the SAT problem,aiming at a series of problems caused by the mutual independence of software and hardware parts in the current solution framework of the software and hardware co-processing,the ZYNQ platform that integrates the ARM processor and the Field Programmable Logic Gate Array(FPGA)in chip is innovatively introduced,and on this basis,the ZYNQ platform is selected for the platform of the framework of the SAT problem solution.The framework adopts the characteristics of the Instance-Specified Solver and the software and hardware co-design method,mapping the SAT problem to a combinational logic circuit of the Programmable Logic(PL)part of the ZYNQ platform.All the state values corresponding to the variables in the SAT problem are generated through the application program running on the processing system(PS),and finally the SAT problem is solved by through the cooperation of software and hardware.Secondly,this thesis introduces a simple SAT solver system in terms of the proposed SAT problem framework on the ZYNQ platform.The design of the whole system can be divided into two parts: hardware and software.The hardware part firstly completes the encapsulation of the SAT problem,converts an SAT problem into the combinational circuit described by Verilog and encapsulates it into an IP core.Secondly designs the data interaction mechanism between software and hardware,and finally integrates the software and hardware parts of the IP core.The software mainly processes the program that generates all the state values corresponding to the variables in the SAT problem and the driver program of the IP core for an underlying SAT problem.Finally,building the operating environment of the SAT solver system and testing the simple SAT solver system based on the ZYNQ platform.The experiment contains the different types of SAT instances and conducts multiple tests.And the experimental results show that the framework based on the ZYNQ platform with a high feasibility and correctness for solving the SAT problems.