PV1 GRATchecks correctness of SAT solver certificates

SAT solver certificate checking tool

Application domain/field

Type of tool

Metatool?

Expected input

Format:

Internals

GRAT is supposed to be used as follows: you provide a certificate, if this is verified, then you have strong formal guarantees that the solution produced by the SAT solver was actually correct. GRAT consists of two programs gratgen and gratchk. gratgen converts a DRAT certificate to a GRAT certificate. gratchk will check the output of gratgen against the original formula. The soundness of gratchk has been formally proven in Isabelle/HOL.
SAT

Links

Project page: https://www21.in.tum.de/~lammich/grat/

Last commit date

Last update seems to be from December 2018

Related tools

drat-trim, LRAT

ProVerB specific

View/edit source (Markdown)



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