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

NAME

6       kissat - manual page for kissat 1.0.3
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 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)
Impressum