1KISSAT(1) User Commands KISSAT(1)
2
6 kissat - manual page for kissat sc2021
7
9 usage: kissat [ <option> ... ] [ <dimacs> [ <proof> ] ]
10 where '<option>' is one of the following common options:
12 --help print this list of all command line options
14 -h print only reduced list of command line options
16 -f force writing proofs (to existing CNF alike file)
18 -n do not print satisfying assignment
20 -q suppress all messages (see also '--quiet')
22 -s print all statistics (see also '--statistics')
24 -v increase verbose level (see also '--verbose')
26 Further '<option>' can be one of the following less frequent options:
28 --banner
30 print solver information
31 --build
33 print build information
34 --color
36 use colors (default if connected to terminal)
37 --no-color
39 no colors (default if not connected to terminal)
40 --compiler
42 print compiler information
43 --copyright
45 print copyright information
46 --force
48 same as '-f' (force writing proof)
49 --id print 'git' identifier (SHA-1 hash)
51 --range
53 print option range list
54 --relaxed
56 relaxed parsing (ignore DIMACS header)
57 --strict
59 stricter parsing (no empty header lines)
60 --version
62 print version
63 The following solving limits can be enforced:
65 --conflicts=<limit>
67 --decisions=<limit>
69 --time=<seconds>
71 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 The following predefined 'configurations' (option settings) are sup‐
77 ported:
78 --basic
80 basic CDCL solving ('--plain' but no restarts, minimize, reduce)
81 --default
83 default configuration
84 --plain
86 plain CDCL solving without advanced techniques
87 --sat target satisfiable instances ('--target=2 --restartint=50')
89 --unsat
91 target unsatisfiable instances ('--stable=0')
92 Or '<option>' is one of the following long options:
94 --ands=<bool>
96 extract and eliminate and gates [true]
97 --autarky=<bool>
99 enable autarky reasoning [true]
100 --autarkydelay=<bool>
102 delay autarky reasoning [false]
103 --backbone=0..2
105 binary clause backbone (2=eager) [1]
106 --backbonedelay=<bool>
108 delay backbone computation [false]
109 --backboneeffort=0..1e5
111 relative effort in per mille [20]
112 --backbonefocus=<bool>
114 focus on not-yet-tried literals [false]
115 --backbonekeep=<bool>
117 keep backbone candidates [true]
118 --backbonemaxrounds=1...
120 maximum backbone rounds [1e3]
121 --backbonerounds=1...
123 backbone rounds limit [100]
124 --backward=<bool>
126 backward subsumption in BVE [true]
127 --bumpreasons=<bool>
129 bump reason side literals too [true]
130 --bumpreasonslimit=1...
132 relative reason literals limit [10]
133 --bumpreasonsrate=1...
135 decision rate limit [10]
136 --cachesample=<bool>
138 sample cached assignments [true]
139 --chrono=<bool>
141 allow chronological backtracking [true]
142 --chronolevels=0...
144 maximum jumped over levels [100]
145 --compact=<bool>
147 enable compacting garbage collection [true]
148 --compactlim=0..100
150 compact inactive limit (in percent) [10]
151 --decay=1..200
153 per mille scores decay [50]
154 --definitioncores=1..100
156 how many cores [2]
157 --definitions=<bool>
159 extract general definitions [true]
160 --defraglim=50..100
162 usable defragmentation limit in percent [75]
163 --defragsize=10...
165 size defragmentation limit [2^18]
166 --delay=0..10
168 maximum delay (autarky, failed, ...) [2]
169 --eagersubsume=0..100
171 eagerly subsume recently learned clauses [20]
172 --eliminate=<bool>
174 bounded variable elimination (BVE) [true]
175 --eliminatebound=0..2^13
177 maximum elimination bound [16]
178 --eliminateclslim=1...
180 elimination clause size limit [100]
181 --eliminatedelay=<bool>
183 delay variable elimination [false]
184 --eliminateeffort=0..2e3
186 relative effort in per mille [100]
187 --eliminateheap=<bool>
189 use heap to schedule elimination [false]
190 --eliminateinit=0...
192 initial elimination interval [500]
193 --eliminateint=10...
195 base elimination interval [500]
196 --eliminatekeep=<bool>
198 keep elimination candidates [true]
199 --eliminateocclim=0...
201 elimination occurrence limit [1e3]
202 --eliminaterounds=1..1e3
204 elimination rounds limit [2]
205 --emafast=10..1e6
207 fast exponential moving average window [33]
208 --emaslow=100..1e6
210 slow exponential moving average window [1e5]
211 --equivalences=<bool>
213 extract and eliminate equivalence gates [true]
214 --extract=<bool>
216 extract gates in variable elimination [true]
217 --failed=<bool>
219 failed literal probing [true]
220 --failedcont=0..100
222 continue if many failed (in percent) [90]
223 --faileddelay=<bool>
225 delay failed literal probing [true]
226 --failedeffort=0..1e8
228 minimum probe effort [50]
229 --failedrounds=1..100
231 failed literal probing rounds [2]
232 --forcephase=<bool>
234 force initial phase [false]
235 --forward=<bool>
237 forward subsumption in BVE [true]
238 --forwardeffort=0..1e6
240 relative effort in per mille [100]
241 --hyper=<bool>
243 on-the-fly hyper binary resolution [true]
244 --ifthenelse=<bool>
246 extract and eliminate if-then-else gates [true]
247 --incremental=<bool>
249 enable incremental solving [false]
250 --mineffort=0...
252 minimum absolute effort [1e4]
253 --minimize=<bool>
255 learned clause minimization [true]
256 --minimizedepth=1..1e6
258 minimization depth [1e3]
259 --minimizeticks=<bool>
261 count ticks in minimize and shrink [true]
262 --modeconflicts=10..1e8
264 initial focused conflicts limit [1e3]
265 --modeticks=1e3...
267 initial focused ticks limit [1e8]
268 --otfs=<bool>
270 on-the-fly strengthening [true]
271 --phase=<bool>
273 initial decision phase [true]
274 --phasesaving=<bool>
276 enable phase saving [true]
277 --probe=<bool>
279 enable probing [true]
280 --probedelay=<bool>
282 delay probing [false]
283 --probeinit=0...
285 initial probing interval [100]
286 --probeint=2...
288 probing interval [100]
289 --profile=0..4
291 profile level [2]
292 --promote=<bool>
294 promote clauses [true]
295 --quiet=<bool>
297 disable all messages [false]
298 --really=<bool>
300 delay preprocessing after scheduling [true]
301 --reap=<bool>
303 enable radix-heap for shrinking [false]
304 --reduce=<bool>
306 learned clause reduction [true]
307 --reducefraction=10..100
309 reduce fraction in percent [75]
310 --reduceinit=2..1e5
312 initial reduce interval [300]
313 --reduceint=2..1e5
315 base reduce interval [1e3]
316 --reducerestart=0..2
318 restart at reduce (1=stable,2=always) [0]
319 --reluctant=<bool>
321 stable reluctant doubling restarting [true]
322 --reluctantint=2..2^15
324 reluctant interval [2^10]
325 --reluctantlim=0..2^30
327 reluctant limit (0=unlimited) [2^20]
328 --rephase=<bool>
330 reinitialization of decision phases [true]
331 --rephasebest=<bool>
333 rephase best phase [true]
334 --rephaseinit=10..1e5
336 initial rephase interval [1e3]
337 --rephaseint=10..1e5
339 base rephase interval [1e3]
340 --rephaseinverted=<bool>
342 rephase inverted phase [true]
343 --rephaseoriginal=<bool>
345 rephase original phase [true]
346 --rephaseprefix=0...
348 initial 'OI' prefix repetition [1]
349 --rephasewalking=<bool>
351 rephase walking phase [true]
352 --restart=<bool>
354 enable restarts [true]
355 --restartint=1..1e4
357 base restart interval [1]
358 --restartmargin=0..25
360 fast/slow margin in percent [10]
361 --restartreusetrail=<bool> restarts reuse trail [true]
363 --seed=0...
365 random seed [0]
366 --shrink=0..3
368 learned clauses (1=bin,2=lrg,3=rec) [3]
369 --shrinkminimize=<bool>
371 minimize during shrinking [true]
372 --simplify=<bool>
374 enable probing and elimination [true]
375 --stable=0..2
377 enable stable search mode [1]
378 --statistics=<bool>
380 print complete statistics [false]
381 --substitute=<bool>
383 equivalent literal substitution [true]
384 --substituteeffort=1..1e3
386 maximum substitution round effort [10]
387 --substituterounds=1..100
389 maximum substitution rounds [2]
390 --subsumeclslim=1...
392 subsumption clause size limit [1e3]
393 --subsumeocclim=0...
395 subsumption occurrence limit [1e3]
396 --target=0..2
398 target phases (1=stable,2=focused) [1]
399 --ternary=<bool>
401 enable hyper ternary resolution [true]
402 --ternarydelay=<bool>
404 delay hyper ternary resolution [true]
405 --ternaryeffort=0..2e3
407 relative effort in per mille [70]
408 --ternaryheap=<bool>
410 use heap to schedule ternary resolution [true]
411 --ternarymaxadd=0..1e4
413 maximum clauses added in percent [20]
414 --tier1=1..100
416 learned clause tier one glue limit [2]
417 --tier2=1..1e3
419 learned clause tier two glue limit [6]
420 --transitive=<bool>
422 transitive reduction of binary clauses [true]
423 --transitiveeffort=0..2e3
425 relative effort in per mille [20]
426 --transitivekeep=<bool>
428 keep transitivity candidates [true]
429 --tumble=<bool>
431 tumbled external indices order [true]
432 --verbose=0..3
434 verbosity level [0]
435 --vivify=<bool>
437 vivify clauses [true]
438 --vivifyeffort=0..1e3
440 relative effort in per mille [100]
441 --vivifyimply=0..2
443 remove implied redundant clauses [2]
444 --vivifyirred=1..100
446 relative irredundant effort [1]
447 --vivifykeep=<bool>
449 keep vivification candidates [false]
450 --vivifytier1=1..100
452 relative tier1 effort [3]
453 --vivifytier2=1..100
455 relative tier2 effort [6]
456 --walkeffort=0..1e6
458 relative effort in per mille [5]
459 --walkfit=<bool>
461 fit CB value to average clause length [true]
462 --walkinitially=<bool>
464 initial local search [false]
465 --walkreuse=0..2
467 reuse walking results (2=always) [1]
468 --walkweighted=<bool>
470 use clause weights [true]
471 --xors=<bool>
473 extract and eliminate XOR gates [true]
474 --xorsbound=0..2^13
476 minimum elimination bound [1]
477 --xorsclslim=3..31
479 XOR extraction clause size limit [5]
480 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 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 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.
499kissat sc2021 January 2022 KISSAT(1)