PV1 ⊧ GRATchecks correctness of SAT solver certificates

SAT solver certificate checking tool

Application domain/field

• SAT solving
• Certificate checking

Type of tool

Metatool?

Expected input

• SAT problem
• SAT certificate

Format:

• SAT problem: .cnf file (DIMACS format)
• SAT certificate: .sat file

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.