MicroSAT-CUDA

A CUDA porting of MicroSAT https://github.com/marijnheule/microsat

MicroSAT is a simple CDCL SAT solver, originally created by MarijnHeule and Armin Biere. It aims at being very short (300 lines of code in-cluding comments) and has neither position saving nor blocking literals. Based on the CDCL procedure, performs unit propagation using two-watched literals and is extremely fast in solving small formulas.

We made a port for CUDA GPUs, to test its performance in parallel resolution of a large amount of formulas.

The dimacs folder contains SAT and UNSAT formulas in DIMACS format ready to be used with MicroSAT-CUDA. The formulas are generated using a CNF formula generator (CNFgen). A different DIMACS generator can be found at https://toughsat.appspot.com/.

For further details, please refer to report.

Table of Contents

• Getting Started
  • Prerequisites
• Usage
  • Supported params
  • Build and run
  • Utils
• Roadmap
• Contributing
• License
• Contact

Getting Started

To get a local copy up and running follow these simple steps.

Prerequisites

• C compilers
• CUDA drivers, to run nvcc command required for build
• On Windows, you need to install dirent.h which is used to list input files
• An IDE that supports CUDA, for example:
  • Visual Studio with CUDA plugin
  • Eclipse Nsight

Usage

Supported params:

• formulas dir, set the folder containing the dimacs files;
• DB_MAX_MEM, set the memory db used by the solver to store clauses and variable assignments;
• CLAUSE_LEARN_MAX_MEM, set the maxium memory that can ve used for clause learning;
• INITIAL_MAX_LEMMAS, set the initial threshold for lemmas. It directly affects the growth of the clause database;
• GPU_COUNT (only for v3), set the number of GPUs to be used by the solver.

Build and run

There are mainly 3 versions of MicroSAT-CUDA:

• MicroSAT-CUDAv1 (microsat_cuda.cu), which is the first version that uses a different mem area for each formula:

# Build
nvcc -o mcudav1 .\microsat_cuda.cu 

# Run
./mcudav1 <formulas dir> <DB_MAX_MEM> <CLAUSE_LEARN_MAX_MEM> <INITIAL_MAX_LEMMAS>

• MicroSAT-CUDAv2 (microsat_cuda_malloc_opt.cu), which is the second version with some memory optimizations:

# Build
nvcc -o mcudav2 .\microsat_cuda_malloc_opt.cu 

# Run
./mcudav2 <formulas dir> <DB_MAX_MEM> <CLAUSE_LEARN_MAX_MEM> <INITIAL_MAX_LEMMAS>

• MicroSAT-CUDAv3 (microsat_cuda_multi_gpu.cu), which is the v2 adapted for multi-GPU support. If you only need a single-GPU run, please refer to MicroSAT-CUDAv2.

# Build
nvcc -o mcudav3 .\microsat_cuda_multi_gpu.cu 

# Run
./mcudav3 <formulas dir> <DB_MAX_MEM> <CLAUSE_LEARN_MAX_MEM> <INITIAL_MAX_LEMMAS> <GPU_COUNT>

Utils

• In slurm folder, there are the SLURM config files used for the test executed on Iridis 5 cluster.
• In script folder, there are the script that can be used for the replication of the experiment described in the report.

Roadmap

See the open issues for a list of proposed features (and known issues).

Contributing

Contributions are what make the open source community such an amazing place to be learn, inspire, and create. Any contributions you make are greatly appreciated.

1. Fork the Project
2. Create your Feature Branch (git checkout -b feature/AmazingFeature)
3. Commit your Changes (git commit -m 'Add some AmazingFeature')
4. Push to the Branch (git push origin feature/AmazingFeature)
5. Open a Pull Request

License

Distributed under the MIT License. See LICENSE for more information.

Contact

• Giovanni
• Massimo

Project Link: https://github.com/grosa1/microsat-cuda