Research On Accelerating Satisfiability Solver Based On GPU

The practical problems in many areas, such as VLSI design verification, model checking, equivalence checking, automatic test pattern generation, etc., can be deduced to an equivalent Boolean Satisfiability problem. That is, these problems can be converted to the boolean formula with CNF (Conjunction Normal Form) format. Finding the solution satisfying the given boolean formula is called satisfiability solving (short for SAT), which is one of the key challenges of modern theoretical computer science.Driven by the increase of application complexity, such as the software verification, theoretical proof, microprocessor verification, VLSI placement and routing, the scale of problems has grown to tens of millions of magnitude, and existing single serial SAT solving techniques cannot meet the demand. At the same time, the existing parallel SAT algorithms have lots of drawbacks, such as low load balancing, shared memory bottlenecks, communication delay increasing, and the high cost of hardware. Therefore, the design of a new type of high-performance satisfiability algorithm is of great significance.GPU is adequate for parallel processing for large-scale data, with a high computational cost, and is widely used in the general-purpose computing fields. Due to the strong control dependence in existing SAT algorithms, it is difficult to be directly mapped to GPU algorithms. This paper focuses on GPU-based satisfiability solving techniques for solving large-scale problems. Instead of mapping classical DPLL (Davis-Putnam-Logemann-Loveland) directly to GPU, a high-performance GPU-based SAT solving framework is presented, which consists of two steps:1) propose the high-performance GPU-based non-exact solving technology based on local search, get the non-exact solution as close to correct solution by fast convergence of the random local search algorithm; 2) based on the non-exact solution generated in former step, propose exact solving to get the eventual solution with the traditional DPLL algorithm. Then the high-performance GPU-based satisfiability solving technique accomplishes.In the implement of the Local search-based non-exact solving technique, due to the simulated annealing algorithm can jump out of local optimal search, the problem is transformed to mathematical problem and simulated annealing energy function is built. The paper presents simulated annealing algorithm for SAT problems, proposes heuristics in initial solution, neighbor selection according to the characteristics of SAT problems, and implements fine-grained paralleled GPU-based simulated annealing algorithm to get the non-exact solution with fast convergence, since after the problem transforming it is more adequate for GPU computing.In the implement of DPLL-based exact solving, take the non-exact solution generated in the former step as a reference for the selected variable assignment, then solve for the exact solution in the traditional way of exact solving. Based on the characteristics of solving, VSIDS_CF, a new variable selection strategy is proposed, which gives priority to the variables with more occurrences and high conflict probability, can eliminate unsatisfied variable assignments and reduce the search space to improve the performance. By analysis of the characteristics of the existing SAT algorithms, the key part of the algorithm-Boolean propagation (BCP) procedure is extracted, and paralleled on GPU in CUDA programming model to achieve efficient propagation.In the end, experiments are set up for techniques proposed in this paper and the GPU-based satisfiability algorithm, considerate speedup is achieved. For the testcases, the average speedup is 5.948, and the most is 28.24.