Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

What environment was this developed under? #1

Open
Codzart opened this issue Oct 12, 2018 · 1 comment
Open

What environment was this developed under? #1

Codzart opened this issue Oct 12, 2018 · 1 comment

Comments

@Codzart
Copy link

Codzart commented Oct 12, 2018

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

@ichorid
Copy link
Owner

ichorid commented Oct 12, 2018

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:

CudaCheckError();

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants