1KISSAT(1) User Commands KISSAT(1)
2
3
4
6 kissat - manual page for kissat 1.0.3
7
9 usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]
10
11 where '<option>' is one of the following common options:
12
13 --help print this list of all command line options
14
15 -h print only reduced list of command line options
16
17 -f force writing proof (to existing CNF alike file)
18
19 -n do not print satisfying assignment
20
21 -q suppress all messages (see also '--quiet')
22
23 -s print all statistics (see also '--statistics')
24
25 -v increase verbose level (see also '--verbose')
26
27 Further '<option>' can be one of the following less frequent options:
28
29 --banner
30 print solver information
31
32 --color
33 use colors (default if connected to terminal)
34
35 --no-color
36 no colors (default if not connected to terminal)
37
38 --embedded
39 print embedded option list
40
41 --force
42 same as '-f' (force writing proof)
43
44 --id print GIT identifier
45
46 --range
47 print option range list
48
49 --relaxed
50 relaxed parsing (ignore DIMACS header)
51
52 --strict
53 stricter parsing (no empty header lines)
54
55 --version
56 print version and exit
57
58 The following solving limits can be enforced:
59
60 --conflicts=<limit>
61
62 --decisions=<limit>
63
64 Satisfying assignments have by default values for all variables unless
65 '--partial' is specified, then only values are printed for variables
66 which are necessary to satisfy the formula.
67
68 The following predefined option settings are supported:
69
70 --default
71 default configuration
72
73 --sat target satisfiable instances ('--target=2')
74
75 --unsat
76 target unsatisfiable instances ('--stable=0')
77
78 Or '<option>' is one of the following long options:
79
80 --ands=<bool>
81 extract and eliminate and gates [true]
82
83 --autarky=<bool>
84 delay autarky reasoning [true]
85
86 --autarkydelay=<bool>
87 enable autarky reasoning [true]
88
89 --backward=<bool>
90 backward subsumption in BVE [true]
91
92 --bumpreasons=<bool>
93 bump reason side literals too [true]
94
95 --chrono=<bool>
96 allow chronological backtracking [true]
97
98 --chronolevels=0...
99 maximum jumped over levels [100]
100
101 --compact=<bool>
102 enable compacting garbage collection [true]
103
104 --compactlim=0..100
105 compact inactive limit (in percent) [10]
106
107 --decay=1..200
108 per mille scores decay [50]
109
110 --defraglim=50..100
111 usable defragmentation limit in percent [75]
112
113 --defragsize=10...
114 size defragmentation limit [2^18]
115
116 --delay=0..10
117 maximum delay (autarky, failed, ...) [2]
118
119 --eagersubsume=0..100
120 eagerly subsume recently learned clauses [20]
121
122 --eliminate=<bool>
123 bounded variable elimination (BVE) [true]
124
125 --eliminatebound=0..2^13
126 maximum elimination bound [16]
127
128 --eliminateclslim=1...
129 elimination clause size limit [100]
130
131 --eliminatedelay=<bool>
132 delay variable elimination [false]
133
134 --eliminateinit=0...
135 initial elimination interval [500]
136
137 --eliminateint=10...
138 base elimination interval [500]
139
140 --eliminatemaxeff=1..1e6
141 maximum relative efficiency [100]
142
143 --eliminatemineff=0..1e8
144 minimum elimination efficiency [1e6]
145
146 --eliminateocclim=0...
147 elimination occurrence limit [1e3]
148
149 --eliminatereleff=0..2e3
150 relative efficiency in per mille [100]
151
152 --eliminaterounds=1..100
153 elimination rounds limit [2]
154
155 --emafast=10..1e6
156 fast exponential moving average window [33]
157
158 --emaslow=100..1e6
159 slow exponential moving average window [1e5]
160
161 --equivalences=<bool>
162 extract and eliminate equivalence gates [true]
163
164 --extract=<bool>
165 extract gates in variable elimination [true]
166
167 --failed=<bool>
168 failed literal probing [true]
169
170 --faileddelay=<bool>
171 delay failed literal probing [true]
172
173 --failedmaxeff=1..1e5
174 maximum relative efficiency [100]
175
176 --failedmineff=0..1e8
177 minimum probe efficiency [5e5]
178
179 --failedreleff=0..1e3
180 relative efficiency in per mille [2]
181
182 --failedrounds=1..100
183 failed literal probing rounds [2]
184
185 --forcephase=<bool>
186 force initial phase [false]
187
188 --forward=<bool>
189 forward subsumption in BVE [true]
190
191 --hyper=<bool>
192 on-the-fly hyper binary resolution [true]
193
194 --ifthenelse=<bool>
195 extract and eliminate if-then-else gates [true]
196
197 --incremental=<bool>
198 enable incremental solving [false]
199
200 --minimizedepth=1..1e6
201 minimization depth [1e3]
202
203 --modeinit=10..1e8
204 initial mode change interval [1e3]
205
206 --modeint=10..1e8
207 base mode change interval [1e3]
208
209 --otfs=<bool>
210 on-the-fly strengthening [true]
211
212 --phase=<bool>
213 initial decision phase [true]
214
215 --phasesaving=<bool>
216 enable phase saving [true]
217
218 --probe=<bool>
219 enable probing [true]
220
221 --probedelay=<bool>
222 delay probing [false]
223
224 --probeinit=0...
225 initial probing interval [100]
226
227 --probeint=2...
228 probing interval [100]
229
230 --profile=0..4
231 profile level [2]
232
233 --quiet=<bool>
234 disable all messages [false]
235
236 --really=<bool>
237 delay preprocessing after scheduling [true]
238
239 --reduce=<bool>
240 learned clause reduction [true]
241
242 --reducefraction=10..100
243 reduce fraction in percent [75]
244
245 --reduceinit=2..1e5
246 initial reduce interval [300]
247
248 --reduceint=2..1e5
249 base reduce interval [300]
250
251 --reducerestart=0..2
252 restart at reduce (1=stable,2=always) [0]
253
254 --reluctant=<bool>
255 stable reluctant doubling restarting [true]
256
257 --reluctantint=2..2^15
258 reluctant interval [2^10]
259
260 --reluctantlim=0..2^30
261 reluctant limit (0=unlimited) [2^20]
262
263 --rephase=<bool>
264 reinitialization of decision phases [true]
265
266 --rephaseinit=10..1e5
267 initial rephase interval [1e3]
268
269 --rephaseint=10..1e5
270 base rephase interval [1e3]
271
272 --restart=<bool>
273 enable restarts [true]
274
275 --restartint=1..1e4
276 base restart interval [1]
277
278 --restartmargin=0..25
279 fast/slow margin in percent [10]
280
281 --seed=0...
282 random seed [0]
283
284 --simplify=<bool>
285 enable probing and elimination [true]
286
287 --stable=0..2
288 enable stable search mode [1]
289
290 --stablebias=0..1e3
291 stable bias in percent [100]
292
293 --statistics=<bool>
294 print complete statistics [false]
295
296 --substitute=<bool>
297 equivalent literal substitution [true]
298
299 --substitutelim=0...
300 substitute multiple round limit [1e7]
301
302 --substitutemineff=0...
303 minimum efficiency [1e6]
304
305 --substituterounds=1..100
306 maximum substitution rounds [2]
307
308 --subsumeclslim=1...
309 subsumption clause size limit [1e3]
310
311 --subsumemaxeff=1..1e6
312 maximum relative efficiency [100]
313
314 --subsumemineff=0..1e8
315 minimum subsume efficiency [1e6]
316
317 --subsumeocclim=0...
318 subsumption occurrence limit [1e3]
319
320 --subsumereleff=0..1e6
321 relative efficiency in per mille [1e4]
322
323 --target=0..2
324 target phases (1=stable,2=focused) [1]
325
326 --ternary=<bool>
327 enable hyper ternary resolution [true]
328
329 --ternarydelay=<bool>
330 delay hyper ternary resolution [true]
331
332 --ternarymaxadd=0..1e4
333 maximum clauses added in percent [20]
334
335 --ternarymaxeff=1..1e4
336 maximum relative efficiency [100]
337
338 --ternarymineff=0..1e8
339 minimum ternary efficiency [1e6]
340
341 --ternaryreleff=0..2e3
342 relative efficiency in per mille [40]
343
344 --tier1=1..100
345 learned clause tier one glue limit [2]
346
347 --tier2=1..1e3
348 learned clause tier two glue limit [6]
349
350 --transitive=<bool>
351 transitive reduction of binary clauses [true]
352
353 --transitivemaxeff=1..1e4
354 maximum relative efficiency [100]
355
356 --transitivemineff=0..1e8
357 minimum transitive efficiency [1e6]
358
359 --transitivereleff=0..2e3
360 relative efficiency in per mille [20]
361
362 --tumble=<bool>
363 tumbled external indices order [true]
364
365 --verbose=0..3
366 verbosity level [0]
367
368 --vivify=<bool>
369 vivify clauses [true]
370
371 --vivifyimply=0..2
372 remove implied redundant clauses [2]
373
374 --vivifymaxeff=1..1e6
375 maximum relative efficiency [50]
376
377 --vivifymineff=0..1e8
378 minimum vivify efficiency [2e5]
379
380 --vivifyreleff=0..1e3
381 relative efficiency in per mille [2]
382
383 --walkinitially=<bool>
384 initial local search [false]
385
386 --walkmaxeff=1...
387 maximum relative efficiency [100]
388
389 --walkmineff=0...
390 minimum vivify efficiency [1e7]
391
392 --walkreleff=0..1e3
393 relative efficiency in per mille [10]
394
395 --walkrounds=1..1e5
396 rounds per walking phase [1]
397
398 --xors=<bool>
399 extract and eliminate XOR gates [true]
400
401 --xorsbound=0..2^13
402 minimum elimination bound [1]
403
404 --xorsclslim=3..31
405 XOR extraction clause size limit [5]
406
407 Furthermore '<dimacs>' is the input file in DIMACS format. The solver
408 reads from '<stdin>' if '<dimacs>' is unspecified. If the path has a
409 '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix then the solver tries to
410 find a corresponding decompression tool ('bzip2', 'gzip', 'lzma', '7z',
411 or 'xz') to decompress the input file on-the-fly after checking that
412 the input file has the correct format (starts with the corresponding
413 signature bytes).
414
415 If '<proof>' is specified then a proof trace is written to the given
416 file. If the file name is '-' then the proof is written to '<stdout>'.
417 In this case the ASCII version of the DRAT format is used. For real
418 files the binary proof format is used unless '--no-binary' is speciā
419 fied.
420
421 Writing of compressed proof files follows the same principle as reading
422 compressed files. The compression format is based on the file suffix
423 and it is checked that the corresponding compression utility can be
424 found.
425
426
427
428kissat 1.0.3 January 2021 KISSAT(1)