/==============================================================================================================================/ / ParaFROST: A Parallel SAT Solver with GPU-Accelerating Inprocessing / Soft Prerequisites: cuda xz python3.8 pip matplotlib numpy / Hard Prerequisites: CUDA-enabled GPU machine with minimum: / 5.0 compute capability / 16 GB system memory / 12 GB device memory / Ubuntu, at least version 18.04 /==============================================================================================================================/ 0) How to evaluate this artefact? --------------------------------- Unpack the ZIP-file on a machine running Ubuntu, at least version 18.04, equipped with at least (1) NVIDIA GPU. Proceed with step 1 below. ================================================================================================================================ 1) How to install ParaFROST? ---------------------------- - First install all the artefact scripts dependencies by running the command sudo apt install xz sudo apt install python3.8 python3.8-dev python3.8-distutils python3.8-venv python3-pip python3.8 -m pip install -U pip python3.8 -m pip install -U numpy python3.8 -m pip install -U matplotlib - Second install CUDA 11.0 or later, if not already available on your machine. NOTE: The CPU-version of ParaFROST and CaDiCaL do not require CUDA and can be installed directly using the provided make files on any CPU machine with GCC compiler. Installing CUDA --------------- - Install the CUDA driver (450 or later). Run from the command line the following: sudo add-apt-repository ppa:graphics-drivers/ppa sudo apt update sudo apt install nvidia-455 nvidia-455-dev Reboot your machine. You can now verify whether this worked by running: nvidia-smi You should get output similar to this, indicating the presence of your GPU: +-----------------------------------------------------------------------------+ | NVIDIA-SMI 450.66 Driver Version: 450.66 CUDA Version: 11.0 | |-------------------------------+----------------------+----------------------+ | GPU Name Persistence-M| Bus-Id Disp.A | Volatile Uncorr. ECC | | Fan Temp Perf Pwr:Usage/Cap| Memory-Usage | GPU-Util Compute M. | | | | MIG M. | |===============================+======================+======================| | 0 TITAN RTX Off | 00000000:01:00.0 Off | N/A | | 41% 42C P8 36W / 280W | 226MiB / 24220MiB | 0% Default | | | | N/A | +-------------------------------+----------------------+----------------------+ - Next, download and install CUDA using the command: sudo apt install nvidia-cuda-toolkit Folow the instructions given regarding the setting of environment variables PATH and LD_LIBRARY_PATH. How to compile ParaFROST? ------------------------- - ParaFROST (GPU): run the make file in the "artefact/solvers/parafrost_gpu" folder using the command 'make' but make sure you have a CUDA-capable device on your machine and the CUDA toolkit (11.0 or later) installed. - ParaFROST (CPU): run the make file in the "artefact/solvers/parafrost_cpu" folder using the command 'make'. - CaDiCaL: run the make file in the "artefact/solvers/cadical" folder using the command './configure && make' . ================================================================================================================================= 2) How to run ParaFROST? ------------------------ - ParaFROST should be run from the command line (it is located in the "artefact/solvers/parafrost_gpu" folder), and can be run with various solving/simplification options (type -h for help or --helpmore for even more help.) - The input file is in DIMACS format which encodes a SAT formula into an integer-number format. Consult the webpage(http://www.satcompetition.org/2011/format-benchmarks2011.html) for more info.. ================================================================================================================================= 3) Running artefact script to produce the experimental results reported in the paper. ------------------------------------------------------------------------------------- NOTE: Make sure these dependencies are installed on your machine: cuda xz screen python3.8 matplotlib numpy All input files (in DIMACS format) for the experiments are available in the "artefact/benchmarks/[easy][medium][hard]" folders. Each difficulty mode of the benchmark folders has the following characteristics: - easy: has 110 formulas and takes around 3 hour or less to solve within a time limit of 100 seconds per formula. - medium: has 121 formulas and takes around 40 hours or more to solve within a time limit of 1000 seconds per formula. - hard: has 89 formulas and takes around 7 days or more to solve within a time limit of 5000 seconds per formula. Run the "easy.sh" script for example in the "artefact" folder to produce the same figures reported in the paper using the formulas in the "artefact/benchmarks/easy" folder. All figures will be printed in high resolution in PDF format and can be found in the "artefact/figures" folder after the artefact runs successfully. The same applies on "medium.sh" and "hard.sh" scripts. The "all.sh" script runs all benchmarks mentioned above. The GPU Speedup figures (figure 3) will be found in: - "artefact/figures/ve_speedup.pdf" - "artefact/figures/gc_speedup.pdf" The SAT solving figures (figure 4) will be found in: - "artefact/figures/solving_time.pdf" - "artefact/figures/inprocessing_time.pdf" - "artefact/figures/inprocessing_perc.pdf" - "artefact/figures/inprocessing_efficiency.pdf" - "artefact/figures/inprocessing_ere.pdf". =================================================================================================================================