forked from arminbiere/kissat
-
Notifications
You must be signed in to change notification settings - Fork 1
/
manual.txt
164 lines (148 loc) · 8.52 KB
/
manual.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]
where '<option>' is one of the following common options:
--help print this list of all command line options
-h print only reduced list of command line options
-f force writing proofs (to existing CNF alike file)
-n do not print satisfying assignment
-q suppress all messages (see also '--quiet')
-s print all statistics (see also '--statistics')
-v increase verbose level (see also '--verbose')
Further '<option>' can be one of the following less frequent options:
--banner print solver information
--build print build information
--color use colors (default if connected to terminal)
--no-color no colors (default if not connected to terminal)
--compiler print compiler information
--copyright print copyright information
--force same as '-f' (force writing proof)
--id print 'git' identifier (SHA-1 hash)
--range print option range list
--relaxed relaxed parsing (ignore DIMACS header)
--strict stricter parsing (no empty header lines)
--version print version
The following solving limits can be enforced:
--conflicts=<limit>
--decisions=<limit>
--time=<seconds>
Satisfying assignments have by default values for all variables
unless '--partial' is specified, then only values are printed
for variables which are necessary to satisfy the formula.
The following predefined 'configurations' (option settings) are supported:
--basic basic CDCL solving ('--plain' but no restarts, minimize, reduce)
--default default configuration
--plain plain CDCL solving without advanced techniques
--sat target satisfiable instances ('--target=2 --restartint=50')
--unsat target unsatisfiable instances ('--stable=0')
Or '<option>' is one of the following long options:
--ands=<bool> extract and eliminate and gates [true]
--backbone=0..2 binary clause backbone (2=eager) [1]
--backboneeffort=0..1e5 effort in per mille [20]
--backbonemaxrounds=1... maximum backbone rounds [1e3]
--backbonerounds=1... backbone rounds limit [100]
--bump=<bool> enable variable bumping [true]
--bumpreasons=<bool> bump reason side literals too [true]
--bumpreasonslimit=1... relative reason literals limit [10]
--bumpreasonsrate=1... decision rate limit [10]
--chrono=<bool> allow chronological backtracking [true]
--chronolevels=0... maximum jumped over levels [100]
--compact=<bool> enable compacting garbage collection [true]
--compactlim=0..100 compact inactive limit (in percent) [10]
--decay=1..200 per mille scores decay [50]
--definitioncores=1..100 how many cores [2]
--definitions=<bool> extract general definitions [true]
--definitionticks=0... kitten ticks limits [1e6]
--defraglim=50..100 usable defragmentation limit in percent [75]
--defragsize=10... size defragmentation limit [2^18]
--eliminate=<bool> bounded variable elimination (BVE) [true]
--eliminatebound=0..2^13 maximum elimination bound [16]
--eliminateclslim=1... elimination clause size limit [100]
--eliminateeffort=0..2e3 effort in per mille [100]
--eliminateinit=0... initial elimination interval [500]
--eliminateint=10... base elimination interval [500]
--eliminateocclim=0... elimination occurrence limit [2e3]
--eliminaterounds=1..1e4 elimination rounds limit [2]
--emafast=10..1e6 fast exponential moving average window [33]
--emaslow=100..1e6 slow exponential moving average window [1e5]
--equivalences=<bool> extract and eliminate equivalence gates [true]
--extract=<bool> extract gates in variable elimination [true]
--forcephase=<bool> force initial phase [false]
--forward=<bool> forward subsumption in BVE [true]
--forwardeffort=0..1e6 effort in per mille [100]
--ifthenelse=<bool> extract and eliminate if-then-else gates [true]
--incremental=<bool> enable incremental solving [false]
--mineffort=0... minimum absolute effort in millions [10]
--minimize=<bool> learned clause minimization [true]
--minimizedepth=1..1e6 minimization depth [1e3]
--minimizeticks=<bool> count ticks in minimize and shrink [true]
--modeinit=10..1e8 initial focused conflicts limit [1e3]
--otfs=<bool> on-the-fly strengthening [true]
--phase=<bool> initial decision phase [true]
--phasesaving=<bool> enable phase saving [true]
--probe=<bool> enable probing [true]
--probeinit=0... initial probing interval [100]
--probeint=2... probing interval [100]
--profile=0..4 profile level [2]
--promote=<bool> promote clauses [true]
--quiet=<bool> disable all messages [false]
--reduce=<bool> learned clause reduction [true]
--reducefraction=10..100 reduce fraction in percent [75]
--reduceinit=2..1e5 initial reduce interval [1e3]
--reduceint=2..1e5 base reduce interval [1e3]
--reluctant=<bool> stable reluctant doubling restarting [true]
--reluctantint=2..2^15 reluctant interval [2^10]
--reluctantlim=0..2^30 reluctant limit (0=unlimited) [2^20]
--rephase=<bool> reinitialization of decision phases [true]
--rephaseinit=10..1e5 initial rephase interval [1e3]
--rephaseint=10..1e5 base rephase interval [1e3]
--restart=<bool> enable restarts [true]
--restartint=1..1e4 base restart interval [1]
--restartmargin=0..25 fast/slow margin in percent [10]
--seed=0... random seed [0]
--shrink=0..3 learned clauses (1=bin,2=lrg,3=rec) [3]
--simplify=<bool> enable probing and elimination [true]
--stable=0..2 enable stable search mode [1]
--statistics=<bool> print complete statistics [false]
--substitute=<bool> equivalent literal substitution [true]
--substituteeffort=1..1e3 effort in per mille [10]
--substituterounds=1..100 maximum substitution rounds [2]
--subsumeclslim=1... subsumption clause size limit [1e3]
--subsumeocclim=0... subsumption occurrence limit [1e3]
--sweep=<bool> enable SAT sweeping [true]
--sweepclauses=0... environment clauses [2^10]
--sweepdepth=0... environment depth [1]
--sweepeffort=0..1e4 effort in per mille [10]
--sweepfliprounds=0... flipping rounds [1]
--sweepmaxclauses=2... maximum environment clauses [2^12]
--sweepmaxdepth=1... maximum environment depth [2]
--sweepmaxvars=2... maximum environment variables [2^7]
--sweepvars=0... environment variables [2^7]
--target=0..2 target phases (1=stable,2=focused) [1]
--tier1=1..100 learned clause tier one glue limit [2]
--tier2=1..1e3 learned clause tier two glue limit [6]
--tumble=<bool> tumbled external indices order [true]
--verbose=0..3 verbosity level [0]
--vivify=<bool> vivify clauses [true]
--vivifyeffort=0..1e3 effort in per mille [100]
--vivifyirred=1..100 relative irredundant effort [1]
--vivifytier1=1..100 relative tier1 effort [3]
--vivifytier2=1..100 relative tier2 effort [6]
--walkeffort=0..1e6 effort in per mille [50]
--walkinitially=<bool> initial local search [false]
--warmup=<bool> initialize phases by unit propagation [true]
Furthermore '<dimacs>' is the input file in DIMACS format.
The solver reads from '<stdin>' if '<dimacs>' is unspecified.
If the path has a '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix
then the solver tries to find a corresponding decompression
tool ('bzip2', 'gzip', 'lzma', '7z', or 'xz') to decompress
the input file on-the-fly after checking that the input file
has the correct format (starts with the corresponding
signature bytes).
If '<proof>' is specified then a proof trace is written to the
given file. If the file name is '-' then the proof is written
to '<stdout>'. In this case the ASCII version of the DRAT format
is used. For real files the binary proof format is used unless
'--no-binary' is specified.
Writing of compressed proof files follows the same principle
as reading compressed files. The compression format is based
on the file suffix and it is checked that the corresponding
compression utility can be found.