1CADICAL(1) User Commands CADICAL(1)
2
6 cadical - manual page for cadical 1.5.2
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 -r <sol>
62 read solution in competition output format to check consistency
63 of learned clauses during testing and debugging
64 -w <sol>
66 write result including a potential witness solution in competi‐
67 tion format to the given file
68 --colors
70 force colored output
71 --no-colors
73 disable colored output to terminal
74 --no-witness
76 do not print witness (see also '-n' above)
77 --build
79 print build configuration
80 --copyright
82 print copyright information
83 There are pre-defined configurations of advanced internal options:
85 --default
87 set default advanced internal options
88 --plain
90 disable all internal preprocessing options
91 --sat set internal options to target satisfiable instances
93 --unsat
95 set internal options to target unsatisfiable instances
96 Or '<option>' is one of the following advanced internal options:
98 --arena=bool
100 allocate clauses in arena [true]
101 --arenacompact=bool
103 keep clauses compact [true]
104 --arenasort=bool
106 sort clauses in arena [true]
107 --arenatype=1..3
109 1=clause, 2=var, 3=queue [3]
110 --binary=bool
112 use binary proof format [true]
113 --block=bool
115 blocked clause elimination [false]
116 --blockmaxclslim=1..2e9
118 maximum clause size [1e5]
119 --blockminclslim=2..2e9
121 minimum clause size [2]
122 --blockocclim=1..2e9
124 occurrence limit [1e2]
125 --bump=bool
127 bump variables [true]
128 --bumpreason=bool
130 bump reason literals too [true]
131 --bumpreasondepth=1..3
133 bump reason depth [1]
134 --check=bool
136 enable internal checking [false]
137 --checkassumptions=bool
139 check assumptions satisfied [true]
140 --checkconstraint=bool
142 check constraint satisfied [true]
143 --checkfailed=bool
145 check failed literals form core [true]
146 --checkfrozen=bool
148 check all frozen semantics [false]
149 --checkproof=bool
151 check proof internally [true]
152 --checkwitness=bool
154 check witness internally [true]
155 --chrono=0..2
157 chronological backtracking [1]
158 --chronoalways=bool
160 force always chronological [false]
161 --chronolevelim=0..2e9
163 chronological level limit [1e2]
164 --chronoreusetrail=bool
166 reuse trail chronologically [true]
167 --compact=bool
169 compact internal variables [true]
170 --compactint=1..2e9
172 compacting interval [2e3]
173 --compactlim=0..1e3
175 inactive limit per mille [1e2]
176 --compactmin=1..2e9
178 minimum inactive limit [1e2]
179 --condition=bool
181 globally blocked clause elim [false]
182 --conditionint=1..2e9
184 initial conflict interval [1e4]
185 --conditionmaxeff=0..2e9
187 maximum condition efficiency [1e7]
188 --conditionmaxrat=1..2e9
190 maximum clause variable ratio [100]
191 --conditionmineff=0..2e9
193 minimum condition efficiency [1e6]
194 --conditionreleff=1..1e5
196 relative efficiency per mille [100]
197 --cover=bool
199 covered clause elimination [false]
200 --covermaxclslim=1..2e9
202 maximum clause size [1e5]
203 --covermaxeff=0..2e9
205 maximum cover efficiency [1e8]
206 --coverminclslim=2..2e9
208 minimum clause size [2]
209 --covermineff=0..2e9
211 minimum cover efficiency [1e6]
212 --coverreleff=1..1e5
214 relative efficiency per mille [4]
215 --decompose=bool
217 decompose BIG in SCCs and ELS [true]
218 --decomposerounds=1..16
220 number of decompose rounds [2]
221 --deduplicate=bool
223 remove duplicated binaries [true]
224 --eagersubsume=bool
226 subsume recently learned [true]
227 --eagersubsumelim=1..1e3
229 limit on subsumed candidates [20]
230 --elim=bool
232 bounded variable elimination [true]
233 --elimands=bool
235 find AND gates [true]
236 --elimaxeff=0..2e9
238 maximum elimination efficiency [2e9]
239 --elimbackward=bool
241 eager backward subsumption [true]
242 --elimboundmax=-1..2e6
244 maximum elimination bound [16]
245 --elimboundmin=-1..2e6
247 minimum elimination bound [0]
248 --elimclslim=2..2e9
250 resolvent size limit [1e2]
251 --elimequivs=bool
253 find equivalence gates [true]
254 --elimineff=0..2e9
256 minimum elimination efficiency [1e7]
257 --elimint=1..2e9
259 elimination interval [2e3]
260 --elimites=bool
262 find if-then-else gates [true]
263 --elimlimited=bool
265 limit resolutions [true]
266 --elimocclim=0..2e9
268 occurrence limit [1e2]
269 --elimprod=0..1e4
271 elim score product weight [1]
272 --elimreleff=1..1e5
274 relative efficiency per mille [1e3]
275 --elimrounds=1..512
277 usual number of rounds [2]
278 --elimsubst=bool
280 elimination by substitution [true]
281 --elimsum=0..1e4
283 elimination score sum weight [1]
284 --elimxorlim=2..27
286 maximum XOR size [5]
287 --elimxors=bool
289 find XOR gates [true]
290 --emagluefast=1..2e9
292 window fast glue [33]
293 --emaglueslow=1..2e9
295 window slow glue [1e5]
296 --emajump=1..2e9
298 window back-jump level [1e5]
299 --emalevel=1..2e9
301 window back-track level [1e5]
302 --emasize=1..2e9
304 window learned clause size [1e5]
305 --ematrailfast=1..2e9
307 window fast trail [1e2]
308 --ematrailslow=1..2e9
310 window slow trail [1e5]
311 --flush=bool
313 flush redundant clauses [false]
314 --flushfactor=1..1e3
316 interval increase [3]
317 --flushint=1..2e9
319 initial limit [1e5]
320 --forcephase=bool
322 always use initial phase [false]
323 --inprocessing=bool
325 enable inprocessing [true]
326 --instantiate=bool
328 variable instantiation [false]
329 --instantiateclslim=2..2e9 minimum clause size [3]
331 --instantiateocclim=1..2e9 maximum occurrence limit [1]
333 --instantiateonce=bool
335 instantiate each clause once [true]
336 --lucky=bool
338 search for lucky phases [true]
339 --minimize=bool
341 minimize learned clauses [true]
342 --minimizedepth=0..1e3
344 minimization depth [1e3]
345 --phase=bool
347 initial phase [true]
348 --probe=bool
350 failed literal probing [true]
351 --probehbr=bool
353 learn hyper binary clauses [true]
354 --probeint=1..2e9
356 probing interval [5e3]
357 --probemaxeff=0..2e9
359 maximum probing efficiency [1e8]
360 --probemineff=0..2e9
362 minimum probing efficiency [1e6]
363 --probereleff=1..1e5
365 relative efficiency per mille [20]
366 --proberounds=1..16
368 probing rounds [1]
369 --profile=0..4
371 profiling level [2]
372 --quiet=bool
374 disable all messages [false]
375 --radixsortlim=0..2e9
377 radix sort limit [800]
378 --realtime=bool
380 real instead of process time [false]
381 --reduce=bool
383 reduce useless clauses [true]
384 --reduceint=10..1e6
386 reduce interval [300]
387 --reducetarget=10..1e2
389 reduce fraction in percent [75]
390 --reducetier1glue=1..2e9
392 glue of kept learned clauses [2]
393 --reducetier2glue=1..2e9
395 glue of tier two clauses [6]
396 --reluctant=0..2e9
398 reluctant doubling period [1024]
399 --reluctantmax=0..2e9
401 reluctant doubling period [1048576]
402 --rephase=bool
404 enable resetting phase [true]
405 --rephaseint=1..2e9
407 rephase interval [1e3]
408 --report=bool
410 enable reporting [false]
411 --reportall=bool
413 report even if not successful [false]
414 --reportsolve=bool
416 use solving not process time [false]
417 --restart=bool
419 enable restarts [true]
420 --restartint=1..2e9
422 restart interval [2]
423 --restartmargin=0..1e2
425 slow fast margin in percent [10]
426 --restartreusetrail=bool
428 enable trail reuse [true]
429 --restoreall=0..2
431 restore all clauses (2=really) [0]
432 --restoreflush=bool
434 remove satisfied clauses [false]
435 --reverse=bool
437 reverse variable ordering [false]
438 --score=bool
440 use EVSIDS scores [true]
441 --scorefactor=500..1e3
443 score factor per mille [950]
444 --seed=0..2e9
446 random seed [0]
447 --shrink=0..3
449 shrink conflict clause [3]
450 --shrinkreap=bool
452 use a reap for shrinking [true]
453 --shuffle=bool
455 shuffle variables [false]
456 --shufflequeue=bool
458 shuffle variable queue [true]
459 --shufflerandom=bool
461 not reverse but random [false]
462 --shufflescores=bool
464 shuffle variable scores [true]
465 --stabilize=bool
467 enable stabilizing phases [true]
468 --stabilizefactor=101..2e9 phase increase in percent [200]
470 --stabilizeint=1..2e9
472 stabilizing interval [1e3]
473 --stabilizemaxint=1..2e9
475 maximum stabilizing phase [2e9]
476 --stabilizeonly=bool
478 only stabilizing phases [false]
479 --subsume=bool
481 enable clause subsumption [true]
482 --subsumebinlim=0..2e9
484 watch list length limit [1e4]
485 --subsumeclslim=0..2e9
487 clause length limit [1e2]
488 --subsumeint=1..2e9
490 subsume interval [1e4]
491 --subsumelimited=bool
493 limit subsumption checks [true]
494 --subsumemaxeff=0..2e9
496 maximum subsuming efficiency [1e8]
497 --subsumemineff=0..2e9
499 minimum subsuming efficiency [1e6]
500 --subsumeocclim=0..2e9
502 watch list length limit [1e2]
503 --subsumereleff=1..1e5
505 relative efficiency per mille [1e3]
506 --subsumestr=bool
508 strengthen during subsume [true]
509 --target=0..2
511 target phases (1=stable only) [1]
512 --terminateint=0..1e4
514 termination check interval [10]
515 --ternary=bool
517 hyper ternary resolution [true]
518 --ternarymaxadd=0..1e4
520 max clauses added in percent [1e3]
521 --ternarymaxeff=0..2e9
523 ternary maximum efficiency [1e8]
524 --ternarymineff=1..2e9
526 minimum ternary efficiency [1e6]
527 --ternaryocclim=1..2e9
529 ternary occurrence limit [1e2]
530 --ternaryreleff=1..1e5
532 relative efficiency per mille [10]
533 --ternaryrounds=1..16
535 maximum ternary rounds [2]
536 --transred=bool
538 transitive reduction of BIG [true]
539 --transredmaxeff=0..2e9
541 maximum efficiency [1e8]
542 --transredmineff=0..2e9
544 minimum efficiency [1e6]
545 --transredreleff=1..1e5
547 relative efficiency per mille [1e2]
548 --verbose=0..3
550 more verbose messages [0]
551 --vivify=bool
553 vivification [true]
554 --vivifymaxeff=0..2e9
556 maximum efficiency [2e7]
557 --vivifymineff=0..2e9
559 minimum efficiency [2e4]
560 --vivifyonce=0..2
562 vivify once: 1=red, 2=red+irr [0]
563 --vivifyredeff=0..1e3
565 redundant efficiency per mille [75]
566 --vivifyreleff=1..1e5
568 relative efficiency per mille [20]
569 --walk=bool
571 enable random walks [true]
572 --walkmaxeff=0..2e9
574 maximum efficiency [1e7]
575 --walkmineff=0..1e7
577 minimum efficiency [1e5]
578 --walknonstable=bool
580 walk in non-stabilizing phase [true]
581 --walkredundant=bool
583 walk redundant clauses too [false]
584 --walkreleff=1..1e5
586 relative efficiency per mille [20]
587 The internal options have their default value printed in brackets after
589 their description. They can also be used in the form '--<name>' which
590 is equivalent to '--<name>=1' and in the form '--no-<name>' which is
591 equivalent to '--<name>=0'. One can also use 'true' instead of '1',
592 'false' instead of '0', as well as numbers with positive exponent such
593 as '1e3' instead of '1000'.
594 Alternatively option values can also be specified in the header of the
596 DIMACS file, e.g., 'c --elim=false', or through environment variables,
597 such as 'CADICAL_ELIM=false'. The embedded options in the DIMACS file
598 have highest priority, followed by command line options and then values
599 specified through environment variables.
600 The input is read from '<input>' assumed to be in DIMACS format. In‐
602 cremental 'p inccnf' files are supported too with cubes at the end. If
603 '<proof>' is given then a DRAT proof is written to that file.
604 If '<input>' is missing then the solver reads from '<stdin>', also if
606 '-' is used as input path name '<input>'. Similarly,
607 For incremental files each cube is solved in turn. The solver stops at
609 the first satisfied cube if there is one and uses that one for the wit‐
610 ness to print. Conflict and decision limits are applied to each indi‐
611 vidual cube solving call while '-P', '-L' and '-t' remain global. Only
612 if all cubes were unsatisfiable the solver prints the standard unsatis‐
613 fiable solution line ('s UNSATISFIABLE').
614 By default the proof is stored in the binary DRAT format unless the op‐
616 tion '--no-binary' is specified or the proof is written to '<stdout>'
617 and '<stdout>' is connected to a terminal.
618 The input is assumed to be compressed if it is given explicitly and has
620 a '.gz', '.bz2', '.xz' or '.7z' suffix. The same applies to the output
621 file. In order to use compression and decompression the corresponding
622 utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are
623 required and need to be installed on the system. The solver checks
624 file type signatures though and falls back to non-compressed file read‐
625 ing if the signature does not match.
626cadical 1.5.2 July 2022 CADICAL(1)