1DRAT-TRIM(1)                     User Commands                    DRAT-TRIM(1)
2
3
4

NAME

6       drat-trim - manual page for drat-trim %{gitdate}
7

DESCRIPTION

9       usage: drat-trim [INPUT] [<PROOF>] [<option> ...]
10
11       where <option> is one of the following
12
13       -h     print this command line option summary
14
15       -c CORE
16              prints the unsatisfiable core to the file CORE (DIMACS format)
17
18       -a ACTIVE
19              prints the active clauses to the file ACTIVE (DIMACS format)
20
21       -l LEMMAS
22              prints the core lemmas to the file LEMMAS (DRAT format)
23
24       -L LEMMAS
25              prints the core lemmas to the file LEMMAS (LRAT format)
26
27       -r TRACE
28              resolution graph in the TRACE file (TRACECHECK format)
29
30       -t <lim>
31              time limit in seconds (default 40000)
32
33       -u     default unit propatation (i.e., no core-first)
34
35       -f     forward mode for UNSAT
36
37       -v     more verbose output
38
39       -q     suppress all output
40
41       -b     show progress bar
42
43       -O     optimize proof till fixpoint by repeating verification
44
45       -C     compress core lemmas (emit binary proof)
46
47       -D     delete proof file after parsing
48
49       -i     force binary proof parse mode
50
51       -w     suppress warning messages
52
53       -W     exit after first warning
54
55       -p     run in plain mode (i.e., ignore deletion information)
56
57       -R     turn off reduce mode
58
59       -S     run in SAT check mode (forward checking)
60
61       and input and proof are specified as follows
62
63       INPUT  input file in DIMACS format
64
65       PROOF  proof file in DRAT format (stdin if no argument)
66
67
68
69drat-trim 1{gitdate}             November 2022                    DRAT-TRIM(1)
Impressum