Exploiting unexploited computing resources for computational logics

Every new desktop or laptop come equipped with a multicore, programmable graphic processing unit (GPU). The computation power of this kind of unit is fully exploited by some graphical software but GPU is mostly idle during common PC use. Moreover, extra GPUs can be added at a very low price per processor. Such kind of parallelism has been recently exploited by some applications able to split the work into small parallel threads. In this paper we investigate the capabilities of this hardware for search problems, where large threads sometimes need to be delegated to each parallel processors. In particular we deal with the well-known SAT problem and focus on NVIDIA CUDA architecture, one of the most popular platforms for GPU. We experimented several implementing choices and evaluated the results. The most interesting outcome is that with the built-in GPU of a typical office desktop configuration we can reach speed-up of one or even two orders of magnitude