drat2er man page

drat2er ā€” manual page for drat2er 20190307

Synopsis

drat2er [Options] input_formula input_proof [output_proof]

Description

drat2er transforms DRAT proofs into extended-resolution proofs. It takes as input a propositional formula (specified in the DIMCAS format) together with a DRAT proof, and outputs an extended-resolution proof of the formula in either the TRACECHECK format or the DRAT format. The description of this transformation can be found in the paper "Extended Resolution Simulates DRAT" (IJCAR 2018). If no output file is specified, the output is written to the standard output.

Positionals

input_formula TEXT:FILE REQUIRED

Path to a DIMCAS file of the input formula.

input_proof TEXT:FILE REQUIRED

Path to a DRAT file of the input proof.

output_proof FILE

Path for the output proof.

Options

-h,--help

Print this help message and exit

-v,--verbose

Print information about the progress.

-q,--quiet

Suppress all output

-c,--compress

Reduce proof size (increases runtime).

-f,--format TEXT:{drat,tracecheck}

Format of the output proof (default: tracecheck).

Info

July 2019 drat2er 20190307