An effective parallel algorithm based on GPU for 3-SAT

SAT problem solving plays an important role in the field of industrial applications. Most of the problems of SAT competitions come from industry. However, the problems of industrial applications are large in scale and it takes a long time to deal with them. This paper introduces the research progress of SAT problem solving algorithm based on hardware acceleration. Secondly, a GPU based Boolean Constraint Propagation algorithm is implemented based on the 3-SAT-DC algorithm, and a clause-literal association structure for GPU is designed. CUDA programming model is used to design and implement the algorithm. Experimental results show that the new 3-SAT-DC algorithm is better than the original algorithm.