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

NAME

6       kissat - manual page for kissat 3.0.0
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       --forcephase=<bool>
189              force initial phase [false]
190
191       --forward=<bool>
192              forward subsumption in BVE [true]
193
194       --forwardeffort=0..1e6
195              effort in per mille [100]
196
197       --ifthenelse=<bool>
198              extract and eliminate if-then-else gates [true]
199
200       --incremental=<bool>
201              enable incremental solving [false]
202
203       --mineffort=0...
204              minimum absolute effort in millions [10]
205
206       --minimize=<bool>
207              learned clause minimization [true]
208
209       --minimizedepth=1..1e6
210              minimization depth [1e3]
211
212       --minimizeticks=<bool>
213              count ticks in minimize and shrink [true]
214
215       --modeinit=10..1e8
216              initial focused conflicts limit [1e3]
217
218       --otfs=<bool>
219              on-the-fly strengthening [true]
220
221       --phase=<bool>
222              initial decision phase [true]
223
224       --phasesaving=<bool>
225              enable phase saving [true]
226
227       --probe=<bool>
228              enable probing [true]
229
230       --probeinit=0...
231              initial probing interval [100]
232
233       --probeint=2...
234              probing interval [100]
235
236       --profile=0..4
237              profile level [2]
238
239       --promote=<bool>
240              promote clauses [true]
241
242       --quiet=<bool>
243              disable all messages [false]
244
245       --reduce=<bool>
246              learned clause reduction [true]
247
248       --reducefraction=10..100
249              reduce fraction in percent [75]
250
251       --reduceinit=2..1e5
252              initial reduce interval [1e3]
253
254       --reduceint=2..1e5
255              base reduce interval [1e3]
256
257       --reluctant=<bool>
258              stable reluctant doubling restarting [true]
259
260       --reluctantint=2..2^15
261              reluctant interval [2^10]
262
263       --reluctantlim=0..2^30
264              reluctant limit (0=unlimited) [2^20]
265
266       --rephase=<bool>
267              reinitialization of decision phases [true]
268
269       --rephaseinit=10..1e5
270              initial rephase interval [1e3]
271
272       --rephaseint=10..1e5
273              base rephase interval [1e3]
274
275       --restart=<bool>
276              enable restarts [true]
277
278       --restartint=1..1e4
279              base restart interval [1]
280
281       --restartmargin=0..25
282              fast/slow margin in percent [10]
283
284       --seed=0...
285              random seed [0]
286
287       --shrink=0..3
288              learned clauses (1=bin,2=lrg,3=rec) [3]
289
290       --simplify=<bool>
291              enable probing and elimination [true]
292
293       --stable=0..2
294              enable stable search mode [1]
295
296       --statistics=<bool>
297              print complete statistics [false]
298
299       --substitute=<bool>
300              equivalent literal substitution [true]
301
302       --substituteeffort=1..1e3
303              effort in per mille [10]
304
305       --substituterounds=1..100
306              maximum substitution rounds [2]
307
308       --subsumeclslim=1...
309              subsumption clause size limit [1e3]
310
311       --subsumeocclim=0...
312              subsumption occurrence limit [1e3]
313
314       --sweep=<bool>
315              enable SAT sweeping [true]
316
317       --sweepclauses=0...
318              environment clauses [2^10]
319
320       --sweepdepth=0...
321              environment depth [1]
322
323       --sweepeffort=0..1e4
324              effort in per mille [10]
325
326       --sweepfliprounds=0...
327              flipping rounds [1]
328
329       --sweepmaxclauses=2...
330              maximum environment clauses [2^12]
331
332       --sweepmaxdepth=1...
333              maximum environment depth [2]
334
335       --sweepmaxvars=2...
336              maximum environment variables [2^7]
337
338       --sweepvars=0...
339              environment variables [2^7]
340
341       --target=0..2
342              target phases (1=stable,2=focused) [1]
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       --tumble=<bool>
351              tumbled external indices order [true]
352
353       --verbose=0..3
354              verbosity level [0]
355
356       --vivify=<bool>
357              vivify clauses [true]
358
359       --vivifyeffort=0..1e3
360              effort in per mille [100]
361
362       --vivifyirred=1..100
363              relative irredundant effort [1]
364
365       --vivifytier1=1..100
366              relative tier1 effort [3]
367
368       --vivifytier2=1..100
369              relative tier2 effort [6]
370
371       --walkeffort=0..1e6
372              effort in per mille [50]
373
374       --walkinitially=<bool>
375              initial local search [false]
376
377       --warmup=<bool>
378              initialize phases by unit propagation [true]
379
380       Furthermore '<dimacs>' is the input file in DIMACS format.  The  solver
381       reads  from  '<stdin>' if '<dimacs>' is unspecified.  If the path has a
382       '.bz2', '.gz', '.lzma', '7z' or '.xz' suffix then the solver  tries  to
383       find a corresponding decompression tool ('bzip2', 'gzip', 'lzma', '7z',
384       or 'xz') to decompress the input file on-the-fly  after  checking  that
385       the  input  file  has the correct format (starts with the corresponding
386       signature bytes).
387
388       If '<proof>' is specified then a proof trace is written  to  the  given
389       file.  If the file name is '-' then the proof is written to '<stdout>'.
390       In this case the ASCII version of the DRAT format is  used.   For  real
391       files  the  binary  proof format is used unless '--no-binary' is speci‐
392       fied.
393
394       Writing of compressed proof files follows the same principle as reading
395       compressed  files.  The  compression format is based on the file suffix
396       and it is checked that the corresponding  compression  utility  can  be
397       found.
398
399
400
401kissat 3.0.0                       July 2022                         KISSAT(1)