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