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

Type of tool

SAT solver

Expected output

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


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


Related papers

Last publication date

15 July 2021

Related tools

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

ProVerB specific

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