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,