一个原型并行完全布尔可满足性（SAT）求解器用CUDA。

This page hosts my source code and Master Thesis of "Implementation of Parallel Boolean Satisfiability Solver by CUDA (Compute Unified Device Architecture)" finished in July, 2011. My source code is not polished, but it works as a complete CDCL DPLL SAT solver with clause-sharing to solve SAT and UNSAT cases. Its performance is about 10,000x slower than MiniSat 2.2.0. My thesis and source code is available in Download section. No development or maintenance would be available for this project since I"m not working with CUDA anymore.