Design And Implementation Of SAT Solver Based On Software And Hardware Cooperative Computing

The Boolean Satisfiability Problem(SAT)is a well-known decision problem and the first NP problem discovered in history.It has been proved that many real problems can be transformed into SAT,such as planning and scheduling in artificial intelligence,model detection and verification in integrated circuits,etc.SAT has always been a research hotspot in the field of theoretical computer science.With the continuous improvement of effort for solving SAT problems,the software solvers have become mature and has very superior performance.However,it is still difficult to effectively solve some types of SAT instances.With the continuous development of integrated circuit technology,the progress of hardware solvers has also promoted.Although the hardware-based solution method has some limitations in the implementation of complex algorithms,it can make full use of the characteristics and resources of the hardware platform to parallelize some modules of the algorithm,so as to realize the SAT solver with reconfigurable hardware.According to the characteristics of the two types of SAT solvers,this paper adopts the application-based hardware solution.Firstly,the random sorting and assignment strategies are merged to the traditional DPLL algorithm to accelerate the solution.We use asynchronous circuit mechanism for a high-performance reconfigurable bidirectional chain circuit that can go forward and backward during assignment.Moreover,the Boolean constraint propagation technique is used to accelerate the derivation process of variables.By analyzing the principle of implicational reasoning,we develop a parser to automatically generate implication formulas of different SAT problems.Secondly,in order to deal with the synchronization between the main processor and coprocessor,as well as long-time communication of the software and hardware,we use the ZYNQ platform that combines CPU with FPGA.The modules that are not related to a specific SAT problem are placed on hardware for parallel acceleration,and the modules related are placed on software for easy configuration and modification.CPU and FPGA communicate through AXI bus.Finally,we design and implement a SAT solver based on software and hardware runtime cooperative computing.Since our hardware part is a reconfigurable computing architecture that can solve up to 200 variables,we only need to configure the software part for the different SAT problems,thus avoiding time-consuming steps such as FPGA synthesis,placement and routing for each SAT instance.We show the test results of many cases and comparison with some software solver.