This project suggest exploring the use of existing implementations of an SDP solution procedure, and swap out the BLAS and LAPACK libraries with their CUDA/GPGPU counterparts. For example, using “libnvblas.so” for the BLAS implementation. The target problem corpus will be "hard" random UNSAT problems in the 3-SAT family, with upwards of 700 Boolean variables.
[*A] Anjos, M. An improved semidefinite programming relaxation for the satisfiability problem. Math. Program. 102, 589–608 (2005).
Boolean Satisfiability, GPGPU, Semidefinite Programming