ParaFROST

ParaFROST stands for Parallel Formal Reasoning On SaTisfiability. It is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in applying modern inprocessing tecnhiques in parallel. The CDCL search is built from scratch with various optimisations based on CaDiCaL heuristics (see our paper in TACAS'21). The inprocessing engine extends our previous work in SIGmA simplifier with new data structures, parallel garbage collection and more.

Install

To install either the CPU or the GPU solvers, use the install.sh script which has the following usage:

  usage: install.sh [ <option> ... ]
  where <option> is one of the following

   -h or --help          print this usage summary
   -n or --less          print less verbose messages
   -q or --quiet         be quiet (make steps still be saved in the log)
   -c or --cpu           install CPU solver
   -g or --gpu           install GPU solver (if CUDA exists)
   -w or --wall          compile with '-Wall' flag
   -d or --debug         compile with debugging inf|ormation
   -t or --assert        enable only code assertions
   -p or --pedantic      compile with '-pedantic' flag
   -l or --logging       enable logging (needed for verbosity level > 2)
   -s or --statistics    enable costly statistics (may impact runtime)
   -a or --all           enable all above flags except 'assert'
   --clean=<target>      remove old installation of <cpu | gpu | all> solvers
   --standard=<n>        compile with <11 | 14 | 17 > c++ standard
   --extra="flags"       pass extra "flags" to the compiler(s)

GPU solver

To build the GPU solver, make sure you have a CUDA-capable GPU with pre-installed NVIDIA driver and CUDA toolkit.

For installing the driver + CUDA, run the following commands:

wget https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/cuda-ubuntu1804.pin
sudo mv cuda-ubuntu1804.pin /etc/apt/preferences.d/cuda-repository-pin-600
sudo apt-key adv --fetch-keys https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/7fa2af80.pub
sudo add-apt-repository "deb https://developer.download.nvidia.com/compute/cuda/repos/ubuntu1804/x86_64/ /"
sudo apt-get update
sudo apt-get -y install cuda

Now the GPU solver is ready to install by running the install script via the command ./install.sh -g. The parafrost binary and the library libparafrost.a will be created by default in the build directory.

CPU solver

To build a CPU-only version of the solver, run ./install.sh -c.

Debug and Testing

Add -t argument with the install command to enable assertions or -d to collect debugging information for both the CPU and GPU solvers.

The solver has a complete artifact for performance evaluation and comparisons with CaDiCaL solver.
More information can be found in: https://gears.win.tue.nl/software/parafrost

Usage

The solver can be used via the command parafrost [<option> ...][<infile>.<cnf>][<option> ...].
For more options, type parafrost -h or parafrost --helpmore.