1CADICAL(1) User Commands CADICAL(1)
2
6 cadical - manual page for cadical 1.0.3
7
9 usage: cadical [ <option> ... ] [ <dimacs> [ <proof> ] ]
10 where '<option>' is one of the following common options
12 -h list of common options
14 --help list of advanced options
16 --version
18 print version
19 -n do not print witness (same as '--no-witness')
21 -v increase verbosity (see also '--verbose')
23 -q be quiet (same as '--quiet')
25 -t <sec>
27 set wall clock time limit
28 or one of the less common options
30 -O<level>
32 increase limits by '10^<level>' (default level '0')
33 -P<rounds>
35 enable preprocessing initially (default '0' rounds)
36 -L<rounds>
38 run local search initialially (default '0' rounds)
39 -c <limit>
41 limit the number of conflicts (default unlimited)
42 -d <limit>
44 limit the number of decisions (default unlimited)
45 -o <dimacs>
47 write simplified CNF in DIMACS format to file
48 -e <extend>
50 write reconstruction/extension stack to file
51 -f | --force
53 parse completely broken DIMACS header
54 --strict
56 enforce strict parsing
57 -s <sol>
59 read solution in competition output format to check consistency
60 of learned clauses during testing and debugging
61 --colors
63 force colored output
64 --no-colors
66 disable colored output to terminal
67 --no-witness
69 do not print witness (see also '-n' above)
70 --build
72 print build configuration
73 --copyright
75 print copyright information
76 or '<option>' is one of the following advanced internal options
78 --arena=bool
80 allocate clauses in arena [true]
81 --arenacompact=bool
83 keep clauses compact [true]
84 --arenasort=bool
86 sort clauses in arena [true]
87 --arenatype=1..3
89 1=clause, 2=var, 3=queue [3]
90 --binary=bool
92 use binary proof format [true]
93 --block=bool
95 blocked clause elimination [false]
96 --blockmaxclslim=1..1e9
98 maximum clause size [1e3]
99 --blockminclslim=2..1e9
101 minimum clause size [2]
102 --blockocclim=1..1e9
104 occurrence limit [1e2]
105 --bump=bool
107 bump variables [true]
108 --bumpreason=bool
110 bump reason literals too [true]
111 --bumpreasondepth=1..3
113 bump reason depth [1]
114 --check=bool
116 enable internal checking [false]
117 --checkassumptions=bool
119 check assumptions satisfied [true]
120 --checkfailed=bool
122 check failed literals form core [true]
123 --checkfrozen=bool
125 check all frozen semantics [false]
126 --checkproof=bool
128 check proof internally [true]
129 --checkwitness=bool
131 check witness internally [true]
132 --chrono=0..2
134 chronological backtracking [1]
135 --chronoalways=bool
137 force always chronological [false]
138 --chronolevelim=0..1e9
140 chronological level limit [1e2]
141 --chronoreusetrail=bool
143 reuse trail chronologically [true]
144 --compact=bool
146 compact internal variables [true]
147 --compactint=1..1e9
149 compacting interval [2e3]
150 --compactlim=0..1e3
152 inactive limit in per mille [1e2]
153 --compactmin=1..1e9
155 minimum inactive limit [1e2]
156 --cover=bool
158 covered clause elimination [false]
159 --covermaxeff=0..1e9
161 maximum cover efficiency [1e8]
162 --covermineff=0..1e9
164 minimum cover efficiency [1e6]
165 --coverreleff=0..1e3
167 relative efficiency per mille [4]
168 --decompose=bool
170 decompose BIG in SCCs and ELS [true]
171 --decomposerounds=1..16
173 number of decompose rounds [2]
174 --deduplicate=bool
176 remove duplicated binary clauses [true]
177 --eagersubsume=bool
179 subsume eagerly recently learned [true]
180 --eagersubsumelim=1..1e3
182 limit on subsumed candidates [20]
183 --elim=bool
185 bounded variable elimination [true]
186 --elimands=bool
188 find AND gates [true]
189 --elimaxeff=0..1e9
191 maximum elimination efficiency [1e9]
192 --elimbackward=bool
194 eager backward subsumption [true]
195 --elimboundmax=-1..256
197 maximum elimination bound [16]
198 --elimboundmin=-1..1e3
200 minimum elimination bound [0]
201 --elimclslim=2..1e9
203 resolvent size limit [1e2]
204 --elimequivs=bool
206 find equivalence gates [true]
207 --elimineff=0..1e9
209 minimum elimination efficiency [1e7]
210 --elimint=1..1e9
212 elimination interval [2e3]
213 --elimites=bool
215 find if-then-else gates [true]
216 --elimlimited=bool
218 limit resolutions [true]
219 --elimocclim=0..1e9
221 occurrence limit [1e3]
222 --elimprod=0..1e4
224 elimination score product [1]
225 --elimreleff=0..1e4
227 relative efficiency per mille [1e3]
228 --elimrounds=1..512
230 usual number of rounds [2]
231 --elimsubst=bool
233 elimination by substitution [true]
234 --elimxorlim=2..27
236 maximum XOR size [5]
237 --elimxors=bool
239 find XOR gates [true]
240 --emagluefast=1..1e9
242 window fast glue [33]
243 --emaglueslow=1..1e9
245 window slow glue [1e5]
246 --emajump=1..1e9
248 window back-jump level [1e5]
249 --emalevel=1..1e9
251 window back-track level [1e5]
252 --emasize=1..1e9
254 window learned clause size [1e5]
255 --ematrailfast=1..1e9
257 window fast trail [1e2]
258 --ematrailslow=1..1e9
260 window slow trail [1e5]
261 --flush=bool
263 flush redundant clauses [true]
264 --flushfactor=1..1e3
266 interval increase [3]
267 --flushint=1..1e9
269 initial limit [1e5]
270 --forcephase=bool
272 always use initial phase [false]
273 --inprocessing=bool
275 enable inprocessing [true]
276 --instantiate=bool
278 variable instantiation [false]
279 --instantiateclslim=2..1e9 minimum clause size [3]
281 --instantiateocclim=1..1e9 maximum occurrence limit [1]
283 --instantiateonce=bool
285 instantiate each clause once [true]
286 --lucky=bool
288 search for lucky phases [true]
289 --minimize=bool
291 minimize learned clauses [true]
292 --minimizedepth=0..1e3
294 minimization depth [1e3]
295 --phase=bool
297 initial phase [true]
298 --probe=bool
300 failed literal probing [true]
301 --probehbr=bool
303 learn hyper binary clauses [true]
304 --probeint=1..1e9
306 probing interval [5e3]
307 --probemaxeff=0..1e9
309 maximum probing efficiency [1e8]
310 --probemineff=0..1e9
312 minimum probing efficiency [1e6]
313 --probereleff=0..1e3
315 relative efficiency per mille [20]
316 --proberounds=1..16
318 probing rounds [1]
319 --profile=0..4
321 profiling level [2]
322 --quiet=bool
324 disable all messages [false]
325 --radixsortlim=0..1e9
327 radix sort limit [800]
328 --realtime=bool
330 real instead of process time [false]
331 --reduce=bool
333 reduce useless clauses [true]
334 --reduceint=10..1e6
336 reduce interval [300]
337 --reducekeepglue=1..1e9
339 glue of kept learned clauses [3]
340 --reducetarget=10..1e2
342 reduce fraction in percent [75]
343 --reluctant=0..1e9
345 reluctant doubling period [1024]
346 --reluctantmax=0..1e9
348 reluctant doubling period [1048576]
349 --rephase=bool
351 enable resetting phase [true]
352 --rephaseint=1..1e9
354 rephase interval [1e3]
355 --report=bool
357 enable reporting [true]
358 --reportall=bool
360 report even if not successful [false]
361 --reportsolve=bool
363 use solving not process time [false]
364 --restart=bool
366 enable restarts [true]
367 --restartint=1..1e9
369 restart interval [2]
370 --restartmargin=0..1e2
372 slow fast margin in percent [10]
373 --restartreusetrail=bool
375 enable trail reuse [true]
376 --restoreall=0..2
378 restore all clauses (2=really) [0]
379 --restoreflush=bool
381 remove satisfied clauses [false]
382 --reverse=bool
384 reverse variable ordering [false]
385 --score=bool
387 use EVSIDS scores [true]
388 --scorefactor=500..1e3
390 score factor per mille [950]
391 --seed=0..1e9
393 random seed [0]
394 --shuffle=bool
396 shuffle variables [false]
397 --shufflequeue=bool
399 shuffle variable queue [true]
400 --shufflerandom=bool
402 not reverse but random [false]
403 --shufflescores=bool
405 shuffle variable scores [true]
406 --simplify=bool
408 enable simplifier [true]
409 --stabilize=bool
411 enable stabilizing phases [true]
412 --stabilizefactor=101..1e9 phase increase in percent [200]
414 --stabilizeint=1..1e9
416 stabilizing interval [1e3]
417 --stabilizemaxint=1..1e9
419 maximum stabilizing phase [1e9]
420 --stabilizeonly=bool
422 only stabilizing phases [false]
423 --stabilizephase=bool
425 use target variable phase [true]
426 --subsume=bool
428 enable clause subsumption [true]
429 --subsumebinlim=0..1e9
431 watch list length limit [1e4]
432 --subsumeclslim=0..1e9
434 clause length limit [1e3]
435 --subsumeint=1..1e9
437 subsume interval [1e4]
438 --subsumelimited=bool
440 limit subsumption checks [true]
441 --subsumemaxeff=0..1e9
443 maximum subsuming efficiency [1e8]
444 --subsumemineff=0..1e9
446 minimum subsuming efficiency [1e6]
447 --subsumeocclim=0..1e9
449 watch list length limit [1e2]
450 --subsumereleff=0..1e4
452 relative efficiency per mille [1e3]
453 --subsumestr=bool
455 strengthen during subsume [true]
456 --ternary=bool
458 hyper ternary resolution [true]
459 --ternarymaxadd=0..1e4
461 maximum clauses added in percent [1e3]
462 --ternarymaxeff=0..1e9
464 ternary maximum efficiency [1e8]
465 --ternarymineff=1..1e9
467 minimum ternary efficiency [1e6]
468 --ternaryocclim=1..1e9
470 ternary occurrence limit [1e2]
471 --ternaryreleff=0..1e5
473 relative efficiency in per mille [10]
474 --ternaryrounds=1..16
476 maximum ternary rounds [2]
477 --transred=bool
479 transitive reduction of BIG [true]
480 --transredmaxeff=0..1e9
482 maximum efficiency [1e8]
483 --transredmineff=0..1e9
485 minimum efficiency [1e6]
486 --transredreleff=0..1e3
488 relative efficiency per mille [1e2]
489 --verbose=0..3
491 more verbose messages [0]
492 --vivify=bool
494 vivification [true]
495 --vivifymaxeff=0..1e9
497 maximum efficiency [1e8]
498 --vivifymineff=0..1e9
500 minimum efficiency [1e5]
501 --vivifyonce=0..2
503 vivify once: 1=red, 2=red+irr [0]
504 --vivifyredeff=0..1e3
506 redundant efficiency per mille [300]
507 --vivifyreleff=0..1e3
509 relative efficiency per mille [80]
510 --walk=bool
512 enable random walks [true]
513 --walkmaxeff=0..1e9
515 maximum efficiency [1e7]
516 --walkmineff=0..1e7
518 minimum efficiency [1e5]
519 --walknonstable=bool
521 walk in non-stabilizing phase [true]
522 --walkredundant=bool
524 walk redundant clauses too [false]
525 --walkreleff=0..1e3
527 relative efficiency per mille [20]
528 The internal options have their default value printed in brackets after
530 their description. They can also be used in the form '--<name>' which
531 is equivalent to '--<name>=1' and in the form '--no-<name>' which is
532 equivalent to '--<name>=0'. One can also use 'true' instead of '1',
533 'false' instead of '0', as well as numbers with positive exponent such
534 as '1e3' instead of '1000'.
535 Alternatively option values can also be specified in the header of the
537 DIMACS file, e.g., 'c --elim=false', or through environment variables,
538 such as 'CADICAL_ELIM=false'. The embedded options in the DIMACS file
539 have highest priority, followed by command line options and then values
540 specified through environment variables.
541 There are also the following pre-defined configurations of options
543 --sat target satisfiable instances
545 --unsat
547 target unsatisfiable instances
548 The input is read from '<dimacs>' assumed to be in DIMACS format. If
550 '<proof>' is given then a DRAT proof is written to that file.
551 If '<dimacs>' is missing then the solver reads from '<stdin>', also if
553 '-' is used as input path name '<dimacs>'. Similarly, if '-' is speci‐
554 fied as '<proof>' path then a proof is generated and printed to '<std‐
555 out>'.
556 By default the proof is stored in the binary DRAT format unless the
558 option '--no-binary' is specified or the proof is written to '<std‐
559 out>' and '<stdout>' is connected to a terminal.
560 The input is assumed to be compressed if it is given explicitly and has
562 a '.gz', '.bz2', '.xz' or '.7z' suffix. The same applies to the output
563 file. In order to use compression and decompression the corresponding
564 utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are
565 required and need to be installed on the system.
566cadical 1.0.3 July 2019 CADICAL(1)