Implementation Of Solving Satisfiability Problem Based On GPU

In computer science,the Boolean satisfiability problem(sometimes called thepropositional satisfaction problem or SAT problem)is a solution to determine whether there is a problem that satisfies a given Boolean formula.In other words,it determines whether the variable of a given boolean formula can be given a TRUE or FALSE truth value,making the final result of the given Boolean formula TRUE.If the final result is TRUE,then we say that the formula is satisfiable.On the other hand,if there is no such allocation,that is,for all possible variable assignments,the result represented by the formula is FALSE,then the formula is said to be unsatisfiable.The SAT was the first problem that proved to be NP-complete.This means that all problems in a complex level NP(including a wide range of natural decisions and optimization issues)are as difficult to solve as SAT.There is no known algorithm that can effectively solve every SAT problem,and it is generally believed that there is no such algorithm,but this belief has not been proved mathematically.This technology is one of the core issues of contemporary theoretical computer science research.The GPU is suitable for large-scale data parallel processing,has a high computational cost performance,and is widely used in the field of general-purpose computing.This paper addresses the needs of solving large-scale problems and studies GPU-based satisfiability solution techniques.Because the classic solver algorithm has a strong control dependence,it is recognized as one of the algorithms that is difficult to be directly mapped to.This article solves the problem in two steps.The first step is to first carry out the inexact solution process.This process uses a combination of genetic algorithm and simulated annealing algorithm.Through the use of this hybrid algorithm,the inaccurate solution that is close to the exact solution is found from the solution space.Step 2: Use the inaccurate solution as an input solution to solve the solution accurately.The algorithm used in this process is the DPLL algorithm.The exact solution to the problem is obtained through the DPLL algorithm to solve the problem.In the inaccurate solution technique based on local search,a mathematic optimization model is established for the satisfiability solving problem.We combine the simulated annealing algorithm and the genetic algorithm,and achieve fine-grained parallelization based on the GPU,and thus efficiently converge to the local optimal solution..In the accurate solution process based on DPLL,the inaccurate solution obtained by the local search in inaccurate solution is used as the reference of the selected variable,and then solved by the traditional exact solution to obtain the final solution.