1KISSAT(1)                        User Commands                       KISSAT(1)
2
3
4

NAME

6       kissat - manual page for kissat sc2021
7

DESCRIPTION

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 proofs (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       --build
33              print build information
34
35       --color
36              use colors (default if connected to terminal)
37
38       --no-color
39              no colors (default if not connected to terminal)
40
41       --compiler
42              print compiler information
43
44       --copyright
45              print copyright information
46
47       --force
48              same as '-f' (force writing proof)
49
50       --id   print 'git' identifier (SHA-1 hash)
51
52       --range
53              print option range list
54
55       --relaxed
56              relaxed parsing (ignore DIMACS header)
57
58       --strict
59              stricter parsing (no empty header lines)
60
61       --version
62              print version
63
64       The following solving limits can be enforced:
65
66       --conflicts=<limit>
67
68       --decisions=<limit>
69
70       --time=<seconds>
71
72       Satisfying  assignments have by default values for all variables unless
73       '--partial' is specified, then only values are  printed  for  variables
74       which are necessary to satisfy the formula.
75
76       The  following  predefined  'configurations' (option settings) are sup‐
77       ported:
78
79       --basic
80              basic CDCL solving ('--plain' but no restarts, minimize, reduce)
81
82       --default
83              default configuration
84
85       --plain
86              plain CDCL solving without advanced techniques
87
88       --sat  target satisfiable instances ('--target=2 --restartint=50')
89
90       --unsat
91              target unsatisfiable instances ('--stable=0')
92
93       Or '<option>' is one of the following long options:
94
95       --ands=<bool>
96              extract and eliminate and gates [true]
97
98       --autarky=<bool>
99              enable autarky reasoning [true]
100
101       --autarkydelay=<bool>
102              delay autarky reasoning [false]
103
104       --backbone=0..2
105              binary clause backbone (2=eager) [1]
106
107       --backbonedelay=<bool>
108              delay backbone computation [false]
109
110       --backboneeffort=0..1e5
111              relative effort in per mille [20]
112
113       --backbonefocus=<bool>
114              focus on not-yet-tried literals [false]
115
116       --backbonekeep=<bool>
117              keep backbone candidates [true]
118
119       --backbonemaxrounds=1...
120              maximum backbone rounds [1e3]
121
122       --backbonerounds=1...
123              backbone rounds limit [100]
124
125       --backward=<bool>
126              backward subsumption in BVE [true]
127
128       --bumpreasons=<bool>
129              bump reason side literals too [true]
130
131       --bumpreasonslimit=1...
132              relative reason literals limit [10]
133
134       --bumpreasonsrate=1...
135              decision rate limit [10]
136
137       --cachesample=<bool>
138              sample cached assignments [true]
139
140       --chrono=<bool>
141              allow chronological backtracking [true]
142
143       --chronolevels=0...
144              maximum jumped over levels [100]
145
146       --compact=<bool>
147              enable compacting garbage collection [true]
148
149       --compactlim=0..100
150              compact inactive limit (in percent) [10]
151
152       --decay=1..200
153              per mille scores decay [50]
154
155       --definitioncores=1..100
156              how many cores [2]
157
158       --definitions=<bool>
159              extract general definitions [true]
160
161       --defraglim=50..100
162              usable defragmentation limit in percent [75]
163
164       --defragsize=10...
165              size defragmentation limit [2^18]
166
167       --delay=0..10
168              maximum delay (autarky, failed, ...) [2]
169
170       --eagersubsume=0..100
171              eagerly subsume recently learned clauses [20]
172
173       --eliminate=<bool>
174              bounded variable elimination (BVE) [true]
175
176       --eliminatebound=0..2^13
177              maximum elimination bound [16]
178
179       --eliminateclslim=1...
180              elimination clause size limit [100]
181
182       --eliminatedelay=<bool>
183              delay variable elimination [false]
184
185       --eliminateeffort=0..2e3
186              relative effort in per mille [100]
187
188       --eliminateheap=<bool>
189              use heap to schedule elimination [false]
190
191       --eliminateinit=0...
192              initial elimination interval [500]
193
194       --eliminateint=10...
195              base elimination interval [500]
196
197       --eliminatekeep=<bool>
198              keep elimination candidates [true]
199
200       --eliminateocclim=0...
201              elimination occurrence limit [1e3]
202
203       --eliminaterounds=1..1e3
204              elimination rounds limit [2]
205
206       --emafast=10..1e6
207              fast exponential moving average window [33]
208
209       --emaslow=100..1e6
210              slow exponential moving average window [1e5]
211
212       --equivalences=<bool>
213              extract and eliminate equivalence gates [true]
214
215       --extract=<bool>
216              extract gates in variable elimination [true]
217
218       --failed=<bool>
219              failed literal probing [true]
220
221       --failedcont=0..100
222              continue if many failed (in percent) [90]
223
224       --faileddelay=<bool>
225              delay failed literal probing [true]
226
227       --failedeffort=0..1e8
228              minimum probe effort [50]
229
230       --failedrounds=1..100
231              failed literal probing rounds [2]
232
233       --forcephase=<bool>
234              force initial phase [false]
235
236       --forward=<bool>
237              forward subsumption in BVE [true]
238
239       --forwardeffort=0..1e6
240              relative effort in per mille [100]
241
242       --hyper=<bool>
243              on-the-fly hyper binary resolution [true]
244
245       --ifthenelse=<bool>
246              extract and eliminate if-then-else gates [true]
247
248       --incremental=<bool>
249              enable incremental solving [false]
250
251       --mineffort=0...
252              minimum absolute effort [1e4]
253
254       --minimize=<bool>
255              learned clause minimization [true]
256
257       --minimizedepth=1..1e6
258              minimization depth [1e3]
259
260       --minimizeticks=<bool>
261              count ticks in minimize and shrink [true]
262
263       --modeconflicts=10..1e8
264              initial focused conflicts limit [1e3]
265
266       --modeticks=1e3...
267              initial focused ticks limit [1e8]
268
269       --otfs=<bool>
270              on-the-fly strengthening [true]
271
272       --phase=<bool>
273              initial decision phase [true]
274
275       --phasesaving=<bool>
276              enable phase saving [true]
277
278       --probe=<bool>
279              enable probing [true]
280
281       --probedelay=<bool>
282              delay probing [false]
283
284       --probeinit=0...
285              initial probing interval [100]
286
287       --probeint=2...
288              probing interval [100]
289
290       --profile=0..4
291              profile level [2]
292
293       --promote=<bool>
294              promote clauses [true]
295
296       --quiet=<bool>
297              disable all messages [false]
298
299       --really=<bool>
300              delay preprocessing after scheduling [true]
301
302       --reap=<bool>
303              enable radix-heap for shrinking [false]
304
305       --reduce=<bool>
306              learned clause reduction [true]
307
308       --reducefraction=10..100
309              reduce fraction in percent [75]
310
311       --reduceinit=2..1e5
312              initial reduce interval [300]
313
314       --reduceint=2..1e5
315              base reduce interval [1e3]
316
317       --reducerestart=0..2
318              restart at reduce (1=stable,2=always) [0]
319
320       --reluctant=<bool>
321              stable reluctant doubling restarting [true]
322
323       --reluctantint=2..2^15
324              reluctant interval [2^10]
325
326       --reluctantlim=0..2^30
327              reluctant limit (0=unlimited) [2^20]
328
329       --rephase=<bool>
330              reinitialization of decision phases [true]
331
332       --rephasebest=<bool>
333              rephase best phase [true]
334
335       --rephaseinit=10..1e5
336              initial rephase interval [1e3]
337
338       --rephaseint=10..1e5
339              base rephase interval [1e3]
340
341       --rephaseinverted=<bool>
342              rephase inverted phase [true]
343
344       --rephaseoriginal=<bool>
345              rephase original phase [true]
346
347       --rephaseprefix=0...
348              initial 'OI' prefix repetition [1]
349
350       --rephasewalking=<bool>
351              rephase walking phase [true]
352
353       --restart=<bool>
354              enable restarts [true]
355
356       --restartint=1..1e4
357              base restart interval [1]
358
359       --restartmargin=0..25
360              fast/slow margin in percent [10]
361
362       --restartreusetrail=<bool> restarts reuse trail [true]
363
364       --seed=0...
365              random seed [0]
366
367       --shrink=0..3
368              learned clauses (1=bin,2=lrg,3=rec) [3]
369
370       --shrinkminimize=<bool>
371              minimize during shrinking [true]
372
373       --simplify=<bool>
374              enable probing and elimination [true]
375
376       --stable=0..2
377              enable stable search mode [1]
378
379       --statistics=<bool>
380              print complete statistics [false]
381
382       --substitute=<bool>
383              equivalent literal substitution [true]
384
385       --substituteeffort=1..1e3
386              maximum substitution round effort [10]
387
388       --substituterounds=1..100
389              maximum substitution rounds [2]
390
391       --subsumeclslim=1...
392              subsumption clause size limit [1e3]
393
394       --subsumeocclim=0...
395              subsumption occurrence limit [1e3]
396
397       --target=0..2
398              target phases (1=stable,2=focused) [1]
399
400       --ternary=<bool>
401              enable hyper ternary resolution [true]
402
403       --ternarydelay=<bool>
404              delay hyper ternary resolution [true]
405
406       --ternaryeffort=0..2e3
407              relative effort in per mille [70]
408
409       --ternaryheap=<bool>
410              use heap to schedule ternary resolution [true]
411
412       --ternarymaxadd=0..1e4
413              maximum clauses added in percent [20]
414
415       --tier1=1..100
416              learned clause tier one glue limit [2]
417
418       --tier2=1..1e3
419              learned clause tier two glue limit [6]
420
421       --transitive=<bool>
422              transitive reduction of binary clauses [true]
423
424       --transitiveeffort=0..2e3
425              relative effort in per mille [20]
426
427       --transitivekeep=<bool>
428              keep transitivity candidates [true]
429
430       --tumble=<bool>
431              tumbled external indices order [true]
432
433       --verbose=0..3
434              verbosity level [0]
435
436       --vivify=<bool>
437              vivify clauses [true]
438
439       --vivifyeffort=0..1e3
440              relative effort in per mille [100]
441
442       --vivifyimply=0..2
443              remove implied redundant clauses [2]
444
445       --vivifyirred=1..100
446              relative irredundant effort [1]
447
448       --vivifykeep=<bool>
449              keep vivification candidates [false]
450
451       --vivifytier1=1..100
452              relative tier1 effort [3]
453
454       --vivifytier2=1..100
455              relative tier2 effort [6]
456
457       --walkeffort=0..1e6
458              relative effort in per mille [5]
459
460       --walkfit=<bool>
461              fit CB value to average clause length [true]
462
463       --walkinitially=<bool>
464              initial local search [false]
465
466       --walkreuse=0..2
467              reuse walking results (2=always) [1]
468
469       --walkweighted=<bool>
470              use clause weights [true]
471
472       --xors=<bool>
473              extract and eliminate XOR gates [true]
474
475       --xorsbound=0..2^13
476              minimum elimination bound [1]
477
478       --xorsclslim=3..31
479              XOR extraction clause size limit [5]
480
481       Furthermore '<dimacs>' is the input file in DIMACS format.  The  solver
482       reads  from  '<stdin>' if '<dimacs>' is unspecified.  If the path has a
483       '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix then the solver  tries  to
484       find a corresponding decompression tool ('bzip2', 'gzip', 'lzma', '7z',
485       or 'xz') to decompress the input file on-the-fly  after  checking  that
486       the  input  file  has the correct format (starts with the corresponding
487       signature bytes).
488
489       If '<proof>' is specified then a proof trace is written  to  the  given
490       file.  If the file name is '-' then the proof is written to '<stdout>'.
491       In this case the ASCII version of the DRAT format is  used.   For  real
492       files  the  binary  proof format is used unless '--no-binary' is speci‐
493       fied.
494
495       Writing of compressed proof files follows the same principle as reading
496       compressed  files.  The  compression format is based on the file suffix
497       and it is checked that the corresponding  compression  utility  can  be
498       found.
499
500
501
502kissat sc2021                    January 2022                        KISSAT(1)
Impressum