ichorid
commented
5 years ago Hi! Thanks for your interest in my work.
The latest version of CUDA that was used during Ringsat development was 8.0. However, this problem you have with cudaCheckError() is really a problem of an old error checking script copy-pasted since CUDA 2.0 or even earlier times. You could just comment out the offending line: https://github.com/ichorid/ringsat/blob/b0ffbcc112d0213c746e44c0a2023965af3e2c5c/solver_cuda.cu#L1029
and it should work fine then (except you lose the error handling).
If you're doing a survey of GPU-based SAT solvers, you could be also interested in my paper describing the reasons why DPLL-based solvers can't run efficiently on modern GPUs. It is written in Russian, but the abstract is in English, and if you don't want to mess around with Google translator, I can tell you the most important points. If you want to cite Ringsat, you could use the abovementioned paper, or the original conference paper.
There is one important thing about SAT-solvers that run BCP procedure on GPU. Their performance really suffers from irregularity of SAT problem, because SIMD architecture is bad at dealing with execution process irregularities, and GPU memory controllers are optimized for coalesced, not random reads. Thus, GPU-based solvers always lose to CPU-based ones in solving generic problems, but really shine in some synthetic tests. One example of these synthetic tests that Ringsat solve really fast is the DUBOIS suite from SATLIB benchmark collection.
Can you briefly describe the NVIDIA toolkit version, GPU card model, etc. that was used during initial development?
I'm trying to stand-up a development system to compile and compare half a dozen published GPU-based 3SAT approaches.
My two hardware contexts are GT 710 and GTX 1070, running within Fedora with NVidia Driver 410.xx and Toolkit 10.x
This code compiles with minor warnings, but upon running the following occurs (paraphrased):
cudaCheckError() failed at ./solver_cuda.cu:1029 invalid configuration argument