Parallel Variable Pre-Selection and Lookahead Solving on GPUs

Christopher Schuster
University of California, Santa Cruz
CMPS 217 Logic in Computer Science, 2014


   title={Parallel Variable Pre-Selection and Lookahead Solving on GPUs},

   author={Schuster, Christopher},



Download Download (PDF)   View View   Source Source   Source codes Source codes




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.
No votes yet.
Please wait...

Recent source codes

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: