13 lines
1.0 KiB
Markdown
13 lines
1.0 KiB
Markdown
# psat
|
|
|
|
Experimental SAT solver using OpenCL on GPU.
|
|
|
|
Make sure that the work group size is set correctly for your GPU (in gpusolver.c). At some point I'll integrate auto-detection, but that day is not today.
|
|
|
|
Plenty of optimizations left to be done, as well as algorithmic changes, particularly to the subsumption check routine.
|
|
|
|
For now the algorithm only operates on a single local workgroup, but it'll be expanded to maintain and run on several independent counters. After that, I plan on integrating work re-balancing: periodically, the work groups will sync with eachother, and in case of a work group having proven its range unsat, the next largest work group will be split between the two.
|
|
|
|
The CPU-bound version of this algorithm is currently about 2x as fast, when I set the local workgroup size to 256. However, the CPU-bound version also takes advantage of early exit scenarios that this algorithm can, but doesn't take advantage of (yet).
|
|
|
|
I'm currently not sure what the best approach is, optimization-wise, out of the ideas I currently have, |