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