drat2er - Man Page
Proof transformer for propositional logic
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.
- -c,--compress
Reduce proof size (increases runtime).
- -f,--format TEXT:{drat,tracecheck}
Format of the output proof (default: tracecheck).