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.

Internals

Based on CaDiCaL, interfaces with CBMC

Comments

NOTE: Although ParaFROST is presented as a parallel SAT solver, it only seems to be available combined with CBMC and thus it is unclear whether it can be used individually without CBMC! License: GPL-3.0
SAT

Links

Last commit date

3 June 2021

Related papers

https://doi.org/10.1007/978-3-030-81688-9_21 (CAV '21)

Last publication date

15 July 2021

Related tools

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

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.