This page contains a link to an artefact we created to experimentally evaluate the effectiveness of the GPU-accelerated Inprocessing integrated to ParaFROST solver v1.0. It is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NIVIDA CUDA-enabled GPUs in applying modern simplification tecnhiques in parallel. The CDCL search is built from scratch with various optimisations based on CaDiCaL heuristics. The inprocessing engine extends our previous work in SIGmA with new data structures, parallel garbage collection and more.

Download and extract the artefact in TACAS21-Artifact. Download and extract the benchmarks contents into the main artefact directory. Follow the instructions in README to run and evaluate the artefact.