high performance computing on graphics processing units: hgpu.org

SAT solving strategies that perform backtracking or clause learning are usually difficult to implement efficiently on massively-parallel architectures because the necessary synchronization does not scale linear with the number of processors available. Strategies like Lookahead Solving and Cube and Conquer are more promising. In order to evaluate a potential GPU implementation of Cube and Conquer, the CPU time spent on Variable ranking and Pre-Selection in the Lookahead Solver march_rw were measured. Both operations can be performed efficiently on GPUs. The results suggest that a wide range of SAT problems involve about 15% of time spent on variable ranking while other problems can be solved without significant work on variable ranking. Future research is necessary to identify more potential targets for parallelization like unit propagation.