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)