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 ASCII proof parse mode
50
51       -i     force binary proof parse mode
52
53       -w     suppress warning messages
54
55       -W     exit after first warning
56
57       -p     run in plain mode (i.e., ignore deletion information)
58
59       -R     turn off reduce mode
60
61       -S     run in SAT check mode (forward checking)
62
63       -U     only allow RUP additions
64
65       and input and proof are specified as follows
66
67       INPUT  input file in DIMACS format
68
69       PROOF  proof file in DRAT format (stdin if no argument)
70
71
72
73drat-trim 1{gitdate}               July 2023                      DRAT-TRIM(1)
Impressum