Man page - drat-trim(1)

Packages contains this manual

Package: drat-trim
apt-get install drat-trim

Manuals in package:

Documentations in package:

drat-trim - DRAT-trim Satisfiability Proof Checker

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)