1DRAT2ER(1)                       User Commands                      DRAT2ER(1)
2
3
4

NAME

6       drat2er - manual page for drat2er 20190307
7

SYNOPSIS

9       drat2er [OPTIONS] input_formula input_proof [output_proof]
10

DESCRIPTION

12       drat2er  transforms  DRAT  proofs  into extended-resolution proofs.  It
13       takes as input a propositional formula (specified in the DIMCAS format)
14       together with a DRAT proof, and outputs an extended-resolution proof of
15       the formula in either the TRACECHECK format or the DRAT format. The de‐
16       scription  of  this  transformation can be found in the paper "Extended
17       Resolution Simulates DRAT" (IJCAR 2018). If no output  file  is  speci‐
18       fied, the output is written to the standard output.
19
20   Positionals:
21       input_formula TEXT:FILE REQUIRED
22              Path to a DIMCAS file of the input formula.
23
24       input_proof TEXT:FILE REQUIRED
25              Path to a DRAT file of the input proof.
26
27       output_proof FILE
28              Path for the output proof.
29

OPTIONS

31       -h,--help
32              Print this help message and exit
33
34       -v,--verbose
35              Print information about the progress.
36
37       -q,--quiet
38              Suppress all output
39
40       -c,--compress
41              Reduce proof size (increases runtime).
42
43       -f,--format TEXT:{drat,tracecheck}
44              Format of the output proof (default: tracecheck).
45
46
47
48drat2er 20190307                 January 2023                       DRAT2ER(1)