clsat

clsat copied to clipboard

clsat - OpenCL SAT solver

clsat is a small, incomplete, stochastic local search, OpenCL-based SAT solver.

The algorithm is as follows:

• Iterate over all the clauses in the instance
• Evaluate each clause under the current valuation
• If a clause is unsatisfied, flip the current value of one of the unsatisfied literals
• Keep going until all the clauses are satisfied

The implementation is designed to work well on GPUs, e.g. by having all threads examine the same clause at the same time, utilising local/shared memory, eliminating branches, etc.

Compiling

You need to have the AMD APP SDK installed to compile and run the program.

$ g++ -Wall -g -I<path/to/AMD-APP-SDK>/include -L<path/to/AMD-APP-SDK>/lib/<arch> main.cc -lOpenCL

To-do

• Split clauses of length > 4 into many smaller clauses
• Support for XOR clauses
• Use u32 for literals (we are currently limited to 32,767 variables)
• Optimisations!
  • Different types may be faster
  • Use vector types/operations if/where possible