GRATgen Documentation

GRATgen is a tool to check DRAT unsatisfiability certificates and convert them into GRAT certificates.

Although GRATgen checks the DRAT certificate during conversion (and also has a check-only mode), its main usage is to generate GRAT certificates which are then checked against the original formula by a formally verified checker.

Author

Peter Lammich

all rights reserved. Some ideas borrowed from Marijn Heule's DRAT-trim tool.

Usage

gratgen cnf-file drat-file [options]

invoke gratgen without arguments to see a list of available options.

Features

Backwards checking with core-first unit propagation
Generation of trimmed GRAT certificates
Parallel checking

Lacking features:

Initially, GRATgen started as a reimplementation of DRAT-trim. Find below a list of features that DRAT-trim has, but GRATgen does not support:

Forward checking (Could be added, but would probably mess up some code)
Binary proof format (Can easily be added)
Optimal deletion placement (Probably not important for GRAT-certificate checking)