Program
Verification
Book

PV4 ⊧ ParaFROSTproduces a satisfiability result for a formula

SAT solver that uses Conflict Driven Clause Learning (CDCL) with GPU acceleration of pre- and inprocessing, tuned for bounded model checking.

Application domain/field

SAT solving
Boolean satisfiability

Type of tool

SAT solver

Expected output

SATISFIABLE, UNSATISFIABLE or an error indicating e.g. out of memory or a timeout.

Internals

Based on CaDiCaL, interfaces with CBMC License: GPL-3.0

Links

Project page: https://gears.win.tue.nl/software/gpu4bmc
ParaFROST Repository: https://github.com/muhos/ParaFROST
- Last commit date: 23 Nov 2022 (default branch)
CBMC Interface Repository: https://github.com/muhos/gpu4bmc
- Last commit date: 14 Mar 2022 (default branch)
Last commit date: 23 Nov 2022 (last activity)

Related papers

SAT Solving with GPU Accelerated Inprocessing (TACAS '21)
GPU Acceleration of Bounded Model Checking with ParaFROST (CAV '21)

Last publication date

15 July 2021

Related tools

Compared to (in CAV '21 paper): MiniSat, Glucose, CaDiCaL

ProVerB specific

Markdown description: view/edit
Reason for this entry: pull request №3
Contained in the ProVerB22 dataset (paper + artefact)

ProVerB is a part of SLEBoK. Last updated: February 2023.