Research On Boolean Satisfiability Solving Technology Based On FPGA Acceleration

Determining the satisfiability of the Boolean formula(SAT)is one of the classic NP-complete problems in computer science.Since practical problems in many fields can be solved by converting into Boolean satisfiable problems,such as VLSI design and verifi-cation,formal verification of software,artificial intelligence planning and optimization,etc.,it has been a research hotspot in the field of computer theory for decades.In re-cent years,with the continuous development of Boolean satisfying solution technology,theSAT solver implemented by software has gradually matured and improved,but for some types ofSAT instances,such as complex 3-SAT instances,there are problems of long learning time and solution efficiency.TheSAT solving technique based on the local search principle and hardware acceleration is the most effective way to improve the effi-ciency of 3-SAT.Therefore,theSAT solving technology based on hardware acceleration has also developed rapidly,which has become a research hotspot in the field of verifica-tion.In recent years,it has been extensively and deeply studied to improve theSAT solv-ing technique based on the principle of random local search.However,the random local search solving technique still has a high improvement potential in general,especially in the solution of the structuredSAT problem.Therefore,the main goal of this paper is to find a new implementation method based on programmable logic devices,in order to solve different types of 3-SAT problems more efficiently and comprehensively,especially the3-SAT random instances.The goal is achieved by the following steps:researching the new analysis method of the initial assignment behavior of the random local search solver,analyzing the preprocessing technique suitable for the random local search solver,and de-signing a new single-threaded random local search hardware solver,and design a parallel multi-threaded random local search hardware solver.Firstly,we analyze the initial assignment of all variables of the problem by traditional SLS solver,and propose aSAT preprocessing algorithm of probabilistic P_ithat the initial assignment of variables is positive in the local search method.The algorithm constrains the parameter value so that when the number of clauses with positive variables is greater than that of negative clauses,the probability of initial assignment is positive is greater than that of negative clauses.Otherwise,the probability is reduced.The algorithm improves the traditional randomly generated initial assignment of variables,makes satisfied clauses as many as possible,which guides the search trend of optimal truth assignment in advance,and improves the convergence speed of the problem greatly.Finally,the phenomenon that the search falls into local optimum is reduced.The algorithm is simple in structure,and can be used in any stochastic local search solver.A field programmable gate array(FPGA)solver called ECWSAT based on enhanced constraint algorithm is proposed,and we apply the probability-based varibale assignment preprocessing technique to the solver.The software preprocessing in the ECWSAT solver is completed by a host computer before the solution begins.The original data of DIMACS format is simplified by using the varibale elimination strategy.All variables are assigned initial values according to the probability,and the corresponding data files are extracted according to the current initial values,such as unsatisfied clauses,address translation table,clause translation table and so on.Finally,all data files are downloaded to the hardware solver.In the main program,we mainly improve the variable selection heuristic and noise disturbance mechanism of the algorithm.In order to avoid the search falling into the local optimum,we introduce a noise disturbance mechanism.When the search enters the local optimum,the algorithm is allowed to select the solution of the same quality or sub-quality as the current candidate solution according to a certain strategy.In order to jump out of the local optimum,the algorithm is put into different optimization directions.The experimental results show that the ECWSAT solver can effectively solve the relatively large scale stochasticSAT problems,especially show good performance in the difficult random problems compared with the softwareSAT solver walksat and other hardware sat solvers.A hardware solver named probsat+based on probability distribution function is pro-posed to solve the problem that the success rate of ECWSAT is not high in solving some large-scale problems.The key of probSAT+solver is a decision heuristic algorithm based on probability distribution function.It only uses the break-value of variables to calculate the distribution of probability.The proposed algorithm is improved in the following three aspects:firstly,in the preprocessing stage,we use the simplified rules of pure literal to determine the initial value of conditional variables;Secondly,the initial assignment of variables is constrained.By guiding the trend of optimal truth-value assignment in ad-vance,the assignment can satisfy as many clauses as possible and reduce the number of flips and the search solution space.Then it reduces the occurrence of local optimum and accelerates the convergence speed of the algorithm.Finally,when we calculate the proba-bility distribution function of variables,we propose a probabilistic solution strategy which is suitable for hardware platform,and avoids complex exponential or polynomial compu-tation in FPGA.Thus the strategy reduces the huge time and area costs.The experimental results show that,compared with walksat and sparrow,which are efficient softwareSAT solver in the industry,probsat+has achieved a larger acceleration ratio and significantly improved the efficiency of solution.A parallel multi-thread solver named pprobsat+based on incomplete algorithm is proposed to improve the throughput of the solver in the search process and enhance the processing capacity of the solver.Based on the probsat+solution framework,the main components of the solver and their interactions are analyzed,and the parallel multi-thread process of the solver and the performance gains brought by the system pipeline are ana-lyzed in detail.The algorithm does not evaluate the result of all clauses,but only evaluates the clauses that will be changed.In other words,the algorithm only evaluates clauses that contain flipping variable,thus the cost of hardware resources is saved greatly.In addition,because of the pipeline design,multiple independent threads are executed simultaneously,which make the parallel and pipeline circuits have higher solution performance.When the instance size is small and all the data is stored on the FPGA chip,the pprobSAT+solver can obtain the maximum performance and speedup.If part of the data can be stored in the off-chip memory,the processing scale of the solver can be greatly increased.The exper-imental results show that pprobsat+can correctly determine the satisfiability of the for-mula,and the three-thread pprobsat+solver can reach more than two times of the speedup compared with the single-thread probsat+solver.