NAME
drat-trim - DRAT-trim Satisfiability Proof Checker
DESCRIPTION
usage: drat-trim [INPUT] [<PROOF>] [<option> ...]
where <option> is one of the following
- -h
-
print this command line option summary
- -c CORE
-
prints the unsatisfiable core to the file CORE (DIMACS format)
- -a ACTIVE
-
prints the active clauses to the file ACTIVE (DIMACS format)
- -l LEMMAS
-
prints the core lemmas to the file LEMMAS (DRAT format)
- -L LEMMAS
-
prints the core lemmas to the file LEMMAS (LRAT format)
- -r TRACE
-
resolution graph in the TRACE file (TRACECHECK format)
- -t <lim>
-
time limit in seconds (default 40000)
- -u
-
default unit propatation (i.e., no core-first)
- -f
-
forward mode for UNSAT
- -v
-
more verbose output
- -b
-
show progress bar
- -O
-
optimize proof till fixpoint by repeating verification
- -C
-
compress core lemmas (emit binary proof)
- -D
-
delete proof file after parsing
- -I
-
force ASCII proof parse mode
- -i
-
force binary proof parse mode
- -w
-
suppress warning messages
- -W
-
exit after first warning
- -p
-
run in plain mode (i.e., ignore deletion information)
- -R
-
turn off reduce mode
- -S
-
run in SAT check mode (forward checking)
- -U
-
only allow RUP additions
and input and proof are specified as follows
- INPUT
-
input file in DIMACS format
- PROOF
-
proof file in DRAT format (stdin if no argument)