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

NAME

6       kissat - manual page for kissat 3.1.1
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       --backbone=0..2
99              binary clause backbone (2=eager) [1]
100
101       --backboneeffort=0..1e5
102              effort in per mille [20]
103
104       --backbonemaxrounds=1...
105              maximum backbone rounds [1e3]
106
107       --backbonerounds=1...
108              backbone rounds limit [100]
109
110       --bump=<bool>
111              enable variable bumping [true]
112
113       --bumpreasons=<bool>
114              bump reason side literals too [true]
115
116       --bumpreasonslimit=1...
117              relative reason literals limit [10]
118
119       --bumpreasonsrate=1...
120              decision rate limit [10]
121
122       --chrono=<bool>
123              allow chronological backtracking [true]
124
125       --chronolevels=0...
126              maximum jumped over levels [100]
127
128       --compact=<bool>
129              enable compacting garbage collection [true]
130
131       --compactlim=0..100
132              compact inactive limit (in percent) [10]
133
134       --decay=1..200
135              per mille scores decay [50]
136
137       --definitioncores=1..100
138              how many cores [2]
139
140       --definitions=<bool>
141              extract general definitions [true]
142
143       --definitionticks=0...
144              kitten ticks limits [1e6]
145
146       --defraglim=50..100
147              usable defragmentation limit in percent [75]
148
149       --defragsize=10...
150              size defragmentation limit [2^18]
151
152       --eliminate=<bool>
153              bounded variable elimination (BVE) [true]
154
155       --eliminatebound=0..2^13
156              maximum elimination bound [16]
157
158       --eliminateclslim=1...
159              elimination clause size limit [100]
160
161       --eliminateeffort=0..2e3
162              effort in per mille [100]
163
164       --eliminateinit=0...
165              initial elimination interval [500]
166
167       --eliminateint=10...
168              base elimination interval [500]
169
170       --eliminateocclim=0...
171              elimination occurrence limit [2e3]
172
173       --eliminaterounds=1..1e4
174              elimination rounds limit [2]
175
176       --emafast=10..1e6
177              fast exponential moving average window [33]
178
179       --emaslow=100..1e6
180              slow exponential moving average window [1e5]
181
182       --equivalences=<bool>
183              extract and eliminate equivalence gates [true]
184
185       --extract=<bool>
186              extract gates in variable elimination [true]
187
188       --flushproof=<bool>
189              flush proof lines immediately [false]
190
191       --forcephase=<bool>
192              force initial phase [false]
193
194       --forward=<bool>
195              forward subsumption in BVE [true]
196
197       --forwardeffort=0..1e6
198              effort in per mille [100]
199
200       --ifthenelse=<bool>
201              extract and eliminate if-then-else gates [true]
202
203       --incremental=<bool>
204              enable incremental solving [false]
205
206       --mineffort=0...
207              minimum absolute effort in millions [10]
208
209       --minimize=<bool>
210              learned clause minimization [true]
211
212       --minimizedepth=1..1e6
213              minimization depth [1e3]
214
215       --minimizeticks=<bool>
216              count ticks in minimize and shrink [true]
217
218       --modeinit=10..1e8
219              initial focused conflicts limit [1e3]
220
221       --modeint=10..1e8
222              focused conflicts interval [1e3]
223
224       --otfs=<bool>
225              on-the-fly strengthening [true]
226
227       --phase=<bool>
228              initial decision phase [true]
229
230       --phasesaving=<bool>
231              enable phase saving [true]
232
233       --probe=<bool>
234              enable probing [true]
235
236       --probeinit=0...
237              initial probing interval [100]
238
239       --probeint=2...
240              probing interval [100]
241
242       --profile=0..4
243              profile level [2]
244
245       --promote=<bool>
246              promote clauses [true]
247
248       --quiet=<bool>
249              disable all messages [false]
250
251       --randec=<bool>
252              random decisions [true]
253
254       --randecfocused=<bool>
255              random decisions in focused mode [true]
256
257       --randecinit=0...
258              random decisions interval [500]
259
260       --randecint=0...
261              initial random decisions interval [500]
262
263       --randeclength=1...
264              random conflicts length [10]
265
266       --randecstable=<bool>
267              random decisions in stable mode [false]
268
269       --reduce=<bool>
270              learned clause reduction [true]
271
272       --reducefraction=10..100
273              reduce fraction in percent [75]
274
275       --reduceinit=2..1e5
276              initial reduce interval [1e3]
277
278       --reduceint=2..1e5
279              base reduce interval [1e3]
280
281       --reluctant=<bool>
282              stable reluctant doubling restarting [true]
283
284       --reluctantint=2..2^15
285              reluctant interval [2^10]
286
287       --reluctantlim=0..2^30
288              reluctant limit (0=unlimited) [2^20]
289
290       --rephase=<bool>
291              reinitialization of decision phases [true]
292
293       --rephaseinit=10..1e5
294              initial rephase interval [1e3]
295
296       --rephaseint=10..1e5
297              base rephase interval [1e3]
298
299       --restart=<bool>
300              enable restarts [true]
301
302       --restartint=1..1e4
303              base restart interval [1]
304
305       --restartmargin=0..25
306              fast/slow margin in percent [10]
307
308       --seed=0...
309              random seed [0]
310
311       --shrink=0..3
312              learned clauses (1=bin,2=lrg,3=rec) [3]
313
314       --simplify=<bool>
315              enable probing and elimination [true]
316
317       --stable=0..2
318              enable stable search mode [1]
319
320       --statistics=<bool>
321              print complete statistics [false]
322
323       --substitute=<bool>
324              equivalent literal substitution [true]
325
326       --substituteeffort=1..1e3
327              effort in per mille [10]
328
329       --substituterounds=1..100
330              maximum substitution rounds [2]
331
332       --subsumeclslim=1...
333              subsumption clause size limit [1e3]
334
335       --subsumeocclim=0...
336              subsumption occurrence limit [1e3]
337
338       --sweep=<bool>
339              enable SAT sweeping [true]
340
341       --sweepclauses=0...
342              environment clauses [2^10]
343
344       --sweepdepth=0...
345              environment depth [2]
346
347       --sweepeffort=0..1e4
348              effort in per mille [100]
349
350       --sweepfliprounds=0...
351              flipping rounds [1]
352
353       --sweepmaxclauses=2...
354              maximum environment clauses [2^15]
355
356       --sweepmaxdepth=1...
357              maximum environment depth [3]
358
359       --sweepmaxvars=2...
360              maximum environment variables [2^13]
361
362       --sweepvars=0...
363              environment variables [2^8]
364
365       --target=0..2
366              target phases (1=stable,2=focused) [1]
367
368       --tier1=1..100
369              learned clause tier one glue limit [2]
370
371       --tier2=1..1e3
372              learned clause tier two glue limit [6]
373
374       --transitive=<bool>
375              transitive reduction of binary clauses [true]
376
377       --transitiveeffort=0..2e3
378              effort in per mille [20]
379
380       --transitivekeep=<bool>
381              keep transitivity candidates [true]
382
383       --tumble=<bool>
384              tumbled external indices order [true]
385
386       --verbose=0..3
387              verbosity level [0]
388
389       --vivify=<bool>
390              vivify clauses [true]
391
392       --vivifyeffort=0..1e3
393              effort in per mille [100]
394
395       --vivifyirr=1..100
396              relative tier1 effort [1]
397
398       --vivifytier1=1..100
399              relative tier1 effort [1]
400
401       --vivifytier2=1..100
402              relative tier2 effort [1]
403
404       --walkeffort=0..1e6
405              effort in per mille [50]
406
407       --walkinitially=<bool>
408              initial local search [false]
409
410       --warmup=<bool>
411              initialize phases by unit propagation [true]
412
413       Furthermore '<dimacs>' is the input file in DIMACS format.  The  solver
414       reads  from  '<stdin>' if '<dimacs>' is unspecified.  If the path has a
415       '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix then the solver  tries  to
416       find a corresponding decompression tool ('bzip2', 'gzip', 'lzma', '7z',
417       or 'xz') to decompress the input file on-the-fly  after  checking  that
418       the  input  file  has the correct format (starts with the corresponding
419       signature bytes).
420
421       If '<proof>' is specified then a proof trace is written  to  the  given
422       file.  If the file name is '-' then the proof is written to '<stdout>'.
423       In this case the ASCII version of the DRAT format is  used.   For  real
424       files  the  binary  proof format is used unless '--no-binary' is speci‐
425       fied.
426
427       Writing of compressed proof files follows the same principle as reading
428       compressed  files.  The  compression format is based on the file suffix
429       and it is checked that the corresponding  compression  utility  can  be
430       found.
431
432
433
434kissat 3.1.1                    September 2023                       KISSAT(1)