1CADICAL(1) User Commands CADICAL(1)
2
6 cadical - manual page for cadical 1.3.0
7
9 usage: cadical [ <option> ... ] [ <input> [ <proof> ] ]
10 where '<option>' is one of the following common options:
12 -h print alternatively only a list of common options
14 --help print this complete list of all options
16 --version
18 print version
19 -n do not print witness (same as '--no-witness')
21 -v increase verbosity (see also '--verbose' below)
23 -q be quiet (same as '--quiet')
25 -t <sec>
27 set wall clock time limit
28 Or '<option>' is one of the less common options
30 -L<rounds>
32 run local search initially (default '0' rounds)
33 -O<level>
35 increase limits by '2^<level>' or '10^<level>'
36 -P<rounds>
38 initial preprocessing (default '0' rounds)
39 Note there is no separating space for the options above while the fol‐
41 lowing options require a space after the option name:
42 -c <limit>
44 limit the number of conflicts (default unlimited)
45 -d <limit>
47 limit the number of decisions (default unlimited)
48 -o <output>
50 write simplified CNF in DIMACS format to file
51 -e <extend>
53 write reconstruction/extension stack to file
54 --force | -f
56 parsing broken DIMACS header and writing proofs
57 --strict
59 strict parsing (no white space in header)
60 -s <sol>
62 read solution in competition output format to check consistency
63 of learned clauses during testing and debugging
64 --colors
66 force colored output
67 --no-colors
69 disable colored output to terminal
70 --no-witness
72 do not print witness (see also '-n' above)
73 --build
75 print build configuration
76 --copyright
78 print copyright information
79 There are pre-defined configurations of advanced internal options:
81 --default
83 set default advanced internal options
84 --plain
86 disable all internal preprocessing options
87 --sat set internal options to target satisfiable instances
89 --unsat
91 set internal options to target unsatisfiable instances
92 Or '<option>' is one of the following advanced internal options:
94 --arena=bool
96 allocate clauses in arena [true]
97 --arenacompact=bool
99 keep clauses compact [true]
100 --arenasort=bool
102 sort clauses in arena [true]
103 --arenatype=1..3
105 1=clause, 2=var, 3=queue [3]
106 --binary=bool
108 use binary proof format [true]
109 --block=bool
111 blocked clause elimination [false]
112 --blockmaxclslim=1..2e9
114 maximum clause size [1e5]
115 --blockminclslim=2..2e9
117 minimum clause size [2]
118 --blockocclim=1..2e9
120 occurrence limit [1e2]
121 --bump=bool
123 bump variables [true]
124 --bumpreason=bool
126 bump reason literals too [true]
127 --bumpreasondepth=1..3
129 bump reason depth [1]
130 --check=bool
132 enable internal checking [false]
133 --checkassumptions=bool
135 check assumptions satisfied [true]
136 --checkfailed=bool
138 check failed literals form core [true]
139 --checkfrozen=bool
141 check all frozen semantics [false]
142 --checkproof=bool
144 check proof internally [true]
145 --checkwitness=bool
147 check witness internally [true]
148 --chrono=0..2
150 chronological backtracking [1]
151 --chronoalways=bool
153 force always chronological [false]
154 --chronolevelim=0..2e9
156 chronological level limit [1e2]
157 --chronoreusetrail=bool
159 reuse trail chronologically [true]
160 --compact=bool
162 compact internal variables [true]
163 --compactint=1..2e9
165 compacting interval [2e3]
166 --compactlim=0..1e3
168 inactive limit per mille [1e2]
169 --compactmin=1..2e9
171 minimum inactive limit [1e2]
172 --condition=bool
174 globally blocked clause elim [false]
175 --conditionint=1..2e9
177 initial conflict interval [1e4]
178 --conditionmaxeff=0..2e9
180 maximum condition efficiency [1e7]
181 --conditionmaxrat=1..2e9
183 maximum clause variable ratio [100]
184 --conditionmineff=0..2e9
186 minimum condition efficiency [1e6]
187 --conditionreleff=1..1e5
189 relative efficiency per mille [100]
190 --cover=bool
192 covered clause elimination [false]
193 --covermaxclslim=1..2e9
195 maximum clause size [1e5]
196 --covermaxeff=0..2e9
198 maximum cover efficiency [1e8]
199 --coverminclslim=2..2e9
201 minimum clause size [2]
202 --covermineff=0..2e9
204 minimum cover efficiency [1e6]
205 --coverreleff=1..1e5
207 relative efficiency per mille [4]
208 --decompose=bool
210 decompose BIG in SCCs and ELS [true]
211 --decomposerounds=1..16
213 number of decompose rounds [2]
214 --deduplicate=bool
216 remove duplicated binaries [true]
217 --eagersubsume=bool
219 subsume recently learned [true]
220 --eagersubsumelim=1..1e3
222 limit on subsumed candidates [20]
223 --elim=bool
225 bounded variable elimination [true]
226 --elimands=bool
228 find AND gates [true]
229 --elimaxeff=0..2e9
231 maximum elimination efficiency [2e9]
232 --elimbackward=bool
234 eager backward subsumption [true]
235 --elimboundmax=-1..2e6
237 maximum elimination bound [16]
238 --elimboundmin=-1..2e6
240 minimum elimination bound [0]
241 --elimclslim=2..2e9
243 resolvent size limit [1e2]
244 --elimequivs=bool
246 find equivalence gates [true]
247 --elimineff=0..2e9
249 minimum elimination efficiency [1e7]
250 --elimint=1..2e9
252 elimination interval [2e3]
253 --elimites=bool
255 find if-then-else gates [true]
256 --elimlimited=bool
258 limit resolutions [true]
259 --elimocclim=0..2e9
261 occurrence limit [1e2]
262 --elimprod=0..1e4
264 elim score product weight [1]
265 --elimreleff=1..1e5
267 relative efficiency per mille [1e3]
268 --elimrounds=1..512
270 usual number of rounds [2]
271 --elimsubst=bool
273 elimination by substitution [true]
274 --elimsum=0..1e4
276 elimination score sum weight [1]
277 --elimxorlim=2..27
279 maximum XOR size [5]
280 --elimxors=bool
282 find XOR gates [true]
283 --emagluefast=1..2e9
285 window fast glue [33]
286 --emaglueslow=1..2e9
288 window slow glue [1e5]
289 --emajump=1..2e9
291 window back-jump level [1e5]
292 --emalevel=1..2e9
294 window back-track level [1e5]
295 --emasize=1..2e9
297 window learned clause size [1e5]
298 --ematrailfast=1..2e9
300 window fast trail [1e2]
301 --ematrailslow=1..2e9
303 window slow trail [1e5]
304 --flush=bool
306 flush redundant clauses [false]
307 --flushfactor=1..1e3
309 interval increase [3]
310 --flushint=1..2e9
312 initial limit [1e5]
313 --forcephase=bool
315 always use initial phase [false]
316 --inprocessing=bool
318 enable inprocessing [true]
319 --instantiate=bool
321 variable instantiation [false]
322 --instantiateclslim=2..2e9 minimum clause size [3]
324 --instantiateocclim=1..2e9 maximum occurrence limit [1]
326 --instantiateonce=bool
328 instantiate each clause once [true]
329 --lucky=bool
331 search for lucky phases [true]
332 --minimize=bool
334 minimize learned clauses [true]
335 --minimizedepth=0..1e3
337 minimization depth [1e3]
338 --phase=bool
340 initial phase [true]
341 --probe=bool
343 failed literal probing [true]
344 --probehbr=bool
346 learn hyper binary clauses [true]
347 --probeint=1..2e9
349 probing interval [5e3]
350 --probemaxeff=0..2e9
352 maximum probing efficiency [1e8]
353 --probemineff=0..2e9
355 minimum probing efficiency [1e6]
356 --probereleff=1..1e5
358 relative efficiency per mille [20]
359 --proberounds=1..16
361 probing rounds [1]
362 --profile=0..4
364 profiling level [2]
365 --quiet=bool
367 disable all messages [false]
368 --radixsortlim=0..2e9
370 radix sort limit [800]
371 --realtime=bool
373 real instead of process time [false]
374 --reduce=bool
376 reduce useless clauses [true]
377 --reduceint=10..1e6
379 reduce interval [300]
380 --reducetarget=10..1e2
382 reduce fraction in percent [75]
383 --reducetier1glue=1..2e9
385 glue of kept learned clauses [2]
386 --reducetier2glue=1..2e9
388 glue of tier two clauses [6]
389 --reluctant=0..2e9
391 reluctant doubling period [1024]
392 --reluctantmax=0..2e9
394 reluctant doubling period [1048576]
395 --rephase=bool
397 enable resetting phase [true]
398 --rephaseint=1..2e9
400 rephase interval [1e3]
401 --report=bool
403 enable reporting [false]
404 --reportall=bool
406 report even if not successful [false]
407 --reportsolve=bool
409 use solving not process time [false]
410 --restart=bool
412 enable restarts [true]
413 --restartint=1..2e9
415 restart interval [2]
416 --restartmargin=0..1e2
418 slow fast margin in percent [10]
419 --restartreusetrail=bool
421 enable trail reuse [true]
422 --restoreall=0..2
424 restore all clauses (2=really) [0]
425 --restoreflush=bool
427 remove satisfied clauses [false]
428 --reverse=bool
430 reverse variable ordering [false]
431 --score=bool
433 use EVSIDS scores [true]
434 --scorefactor=500..1e3
436 score factor per mille [950]
437 --seed=0..2e9
439 random seed [0]
440 --shuffle=bool
442 shuffle variables [false]
443 --shufflequeue=bool
445 shuffle variable queue [true]
446 --shufflerandom=bool
448 not reverse but random [false]
449 --shufflescores=bool
451 shuffle variable scores [true]
452 --stabilize=bool
454 enable stabilizing phases [true]
455 --stabilizefactor=101..2e9 phase increase in percent [200]
457 --stabilizeint=1..2e9
459 stabilizing interval [1e3]
460 --stabilizemaxint=1..2e9
462 maximum stabilizing phase [2e9]
463 --stabilizeonly=bool
465 only stabilizing phases [false]
466 --stabilizephase=bool
468 use target variable phase [true]
469 --subsume=bool
471 enable clause subsumption [true]
472 --subsumebinlim=0..2e9
474 watch list length limit [1e4]
475 --subsumeclslim=0..2e9
477 clause length limit [1e2]
478 --subsumeint=1..2e9
480 subsume interval [1e4]
481 --subsumelimited=bool
483 limit subsumption checks [true]
484 --subsumemaxeff=0..2e9
486 maximum subsuming efficiency [1e8]
487 --subsumemineff=0..2e9
489 minimum subsuming efficiency [1e6]
490 --subsumeocclim=0..2e9
492 watch list length limit [1e2]
493 --subsumereleff=1..1e5
495 relative efficiency per mille [1e3]
496 --subsumestr=bool
498 strengthen during subsume [true]
499 --terminateint=0..1e4
501 termination check interval [10]
502 --ternary=bool
504 hyper ternary resolution [true]
505 --ternarymaxadd=0..1e4
507 max clauses added in percent [1e3]
508 --ternarymaxeff=0..2e9
510 ternary maximum efficiency [1e8]
511 --ternarymineff=1..2e9
513 minimum ternary efficiency [1e6]
514 --ternaryocclim=1..2e9
516 ternary occurrence limit [1e2]
517 --ternaryreleff=1..1e5
519 relative efficiency per mille [10]
520 --ternaryrounds=1..16
522 maximum ternary rounds [2]
523 --transred=bool
525 transitive reduction of BIG [true]
526 --transredmaxeff=0..2e9
528 maximum efficiency [1e8]
529 --transredmineff=0..2e9
531 minimum efficiency [1e6]
532 --transredreleff=1..1e5
534 relative efficiency per mille [1e2]
535 --verbose=0..3
537 more verbose messages [0]
538 --vivify=bool
540 vivification [true]
541 --vivifymaxeff=0..2e9
543 maximum efficiency [2e7]
544 --vivifymineff=0..2e9
546 minimum efficiency [2e4]
547 --vivifyonce=0..2
549 vivify once: 1=red, 2=red+irr [0]
550 --vivifyredeff=0..1e3
552 redundant efficiency per mille [75]
553 --vivifyreleff=1..1e5
555 relative efficiency per mille [20]
556 --walk=bool
558 enable random walks [true]
559 --walkmaxeff=0..2e9
561 maximum efficiency [1e7]
562 --walkmineff=0..1e7
564 minimum efficiency [1e5]
565 --walknonstable=bool
567 walk in non-stabilizing phase [true]
568 --walkredundant=bool
570 walk redundant clauses too [false]
571 --walkreleff=1..1e5
573 relative efficiency per mille [20]
574 The internal options have their default value printed in brackets after
576 their description. They can also be used in the form '--<name>' which
577 is equivalent to '--<name>=1' and in the form '--no-<name>' which is
578 equivalent to '--<name>=0'. One can also use 'true' instead of '1',
579 'false' instead of '0', as well as numbers with positive exponent such
580 as '1e3' instead of '1000'.
581 Alternatively option values can also be specified in the header of the
583 DIMACS file, e.g., 'c --elim=false', or through environment variables,
584 such as 'CADICAL_ELIM=false'. The embedded options in the DIMACS file
585 have highest priority, followed by command line options and then values
586 specified through environment variables.
587 The input is read from '<input>' assumed to be in DIMACS format.
589 Incremental 'p inccnf' files are supported too with cubes at the end.
590 If '<proof>' is given then a DRAT proof is written to that file.
591 If '<input>' is missing then the solver reads from '<stdin>', also if
593 '-' is used as input path name '<input>'. Similarly,
594 For incremental files each cube is solved in turn. The solver stops at
596 the first satisfied cube if there is one and uses that one for the wit‐
597 ness to print. Conflict and decision limits are applied to each indi‐
598 vidual cube solving call while '-P', '-L' and '-t' remain global. Only
599 if all cubes were unsatisfiable the solver prints the standard unsatis‐
600 fiable solution line ('s UNSATISFIABLE').
601 By default the proof is stored in the binary DRAT format unless the
603 option '--no-binary' is specified or the proof is written to '<std‐
604 out>' and '<stdout>' is connected to a terminal.
605 The input is assumed to be compressed if it is given explicitly and has
607 a '.gz', '.bz2', '.xz' or '.7z' suffix. The same applies to the output
608 file. In order to use compression and decompression the corresponding
609 utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are
610 required and need to be installed on the system. The solver checks
611 file type signatures though and falls back to non-compressed file read‐
612 ing if the signature does not match.
613cadical 1.3.0 August 2020 CADICAL(1)