1CADICAL(1) User Commands CADICAL(1)
2
6 cadical - manual page for cadical 1.2.1
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 '{2,10}^<level>' (default '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..2e9
98 maximum clause size [1e5]
99 --blockminclslim=2..2e9
101 minimum clause size [4]
102 --blockocclim=1..2e9
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..2e9
140 chronological level limit [1e2]
141 --chronoreusetrail=bool
143 reuse trail chronologically [true]
144 --compact=bool
146 compact internal variables [true]
147 --compactint=1..2e9
149 compacting interval [2e3]
150 --compactlim=0..1e3
152 inactive limit in per mille [1e2]
153 --compactmin=1..2e9
155 minimum inactive limit [1e2]
156 --condition=bool
158 globally blocked clause elim [false]
159 --conditionint=1..2e9
161 initial conflict interval [1e4]
162 --conditionmaxeff=0..2e9
164 maximum condition efficiency [1e7]
165 --conditionmaxratio=1..2e9 maximum clause variable ratio [100]
167 --conditionmineff=0..2e9
169 minimum condition efficiency [1e6]
170 --conditionreleff=1..1e5
172 relative efficiency in per mille [100]
173 --cover=bool
175 covered clause elimination [false]
176 --covermaxclslim=1..2e9
178 maximum clause size [1e5]
179 --covermaxeff=0..2e9
181 maximum cover efficiency [1e8]
182 --coverminclslim=2..2e9
184 minimum clause size [4]
185 --covermineff=0..2e9
187 minimum cover efficiency [1e6]
188 --coverreleff=1..1e5
190 relative efficiency per mille [4]
191 --decompose=bool
193 decompose BIG in SCCs and ELS [true]
194 --decomposerounds=1..16
196 number of decompose rounds [2]
197 --deduplicate=bool
199 remove duplicated binary clauses [true]
200 --eagersubsume=bool
202 subsume eagerly recently learned [true]
203 --eagersubsumelim=1..1e3
205 limit on subsumed candidates [20]
206 --elim=bool
208 bounded variable elimination [true]
209 --elimands=bool
211 find AND gates [true]
212 --elimaxeff=0..2e9
214 maximum elimination efficiency [2e9]
215 --elimbackward=bool
217 eager backward subsumption [true]
218 --elimboundmax=-1..2e6
220 maximum elimination bound [16]
221 --elimboundmin=-1..2e6
223 minimum elimination bound [0]
224 --elimclslim=2..2e9
226 resolvent size limit [1e2]
227 --elimequivs=bool
229 find equivalence gates [true]
230 --elimineff=0..2e9
232 minimum elimination efficiency [1e7]
233 --elimint=1..2e9
235 elimination interval [2e3]
236 --elimites=bool
238 find if-then-else gates [true]
239 --elimlimited=bool
241 limit resolutions [true]
242 --elimocclim=0..2e9
244 occurrence limit [1e3]
245 --elimprod=0..1e4
247 elimination score product [1]
248 --elimreleff=1..1e5
250 relative efficiency per mille [1e3]
251 --elimrounds=1..512
253 usual number of rounds [2]
254 --elimsubst=bool
256 elimination by substitution [true]
257 --elimxorlim=2..27
259 maximum XOR size [5]
260 --elimxors=bool
262 find XOR gates [true]
263 --emagluefast=1..2e9
265 window fast glue [33]
266 --emaglueslow=1..2e9
268 window slow glue [1e5]
269 --emajump=1..2e9
271 window back-jump level [1e5]
272 --emalevel=1..2e9
274 window back-track level [1e5]
275 --emasize=1..2e9
277 window learned clause size [1e5]
278 --ematrailfast=1..2e9
280 window fast trail [1e2]
281 --ematrailslow=1..2e9
283 window slow trail [1e5]
284 --flush=bool
286 flush redundant clauses [false]
287 --flushfactor=1..1e3
289 interval increase [3]
290 --flushint=1..2e9
292 initial limit [1e5]
293 --forcephase=bool
295 always use initial phase [false]
296 --inprocessing=bool
298 enable inprocessing [true]
299 --instantiate=bool
301 variable instantiation [false]
302 --instantiateclslim=2..2e9 minimum clause size [3]
304 --instantiateocclim=1..2e9 maximum occurrence limit [1]
306 --instantiateonce=bool
308 instantiate each clause once [true]
309 --lucky=bool
311 search for lucky phases [true]
312 --minimize=bool
314 minimize learned clauses [true]
315 --minimizedepth=0..1e3
317 minimization depth [1e3]
318 --phase=bool
320 initial phase [true]
321 --probe=bool
323 failed literal probing [true]
324 --probehbr=bool
326 learn hyper binary clauses [true]
327 --probeint=1..2e9
329 probing interval [5e3]
330 --probemaxeff=0..2e9
332 maximum probing efficiency [1e8]
333 --probemineff=0..2e9
335 minimum probing efficiency [1e6]
336 --probereleff=1..1e5
338 relative efficiency per mille [20]
339 --proberounds=1..16
341 probing rounds [1]
342 --profile=0..4
344 profiling level [2]
345 --quiet=bool
347 disable all messages [false]
348 --radixsortlim=0..2e9
350 radix sort limit [800]
351 --realtime=bool
353 real instead of process time [false]
354 --reduce=bool
356 reduce useless clauses [true]
357 --reduceint=10..1e6
359 reduce interval [300]
360 --reducetarget=10..1e2
362 reduce fraction in percent [75]
363 --reducetier1glue=1..2e9
365 glue of kept learned clauses [2]
366 --reducetier2glue=1..2e9
368 glue of tier two clauses [6]
369 --reluctant=0..2e9
371 reluctant doubling period [1024]
372 --reluctantmax=0..2e9
374 reluctant doubling period [1048576]
375 --rephase=bool
377 enable resetting phase [true]
378 --rephaseint=1..2e9
380 rephase interval [1e3]
381 --report=bool
383 enable reporting [true]
384 --reportall=bool
386 report even if not successful [false]
387 --reportsolve=bool
389 use solving not process time [false]
390 --restart=bool
392 enable restarts [true]
393 --restartint=1..2e9
395 restart interval [2]
396 --restartmargin=0..1e2
398 slow fast margin in percent [10]
399 --restartreusetrail=bool
401 enable trail reuse [true]
402 --restoreall=0..2
404 restore all clauses (2=really) [0]
405 --restoreflush=bool
407 remove satisfied clauses [false]
408 --reverse=bool
410 reverse variable ordering [false]
411 --score=bool
413 use EVSIDS scores [true]
414 --scorefactor=500..1e3
416 score factor per mille [950]
417 --seed=0..2e9
419 random seed [0]
420 --shuffle=bool
422 shuffle variables [false]
423 --shufflequeue=bool
425 shuffle variable queue [true]
426 --shufflerandom=bool
428 not reverse but random [false]
429 --shufflescores=bool
431 shuffle variable scores [true]
432 --simplify=bool
434 enable simplifier [true]
435 --stabilize=bool
437 enable stabilizing phases [true]
438 --stabilizefactor=101..2e9 phase increase in percent [200]
440 --stabilizeint=1..2e9
442 stabilizing interval [1e3]
443 --stabilizemaxint=1..2e9
445 maximum stabilizing phase [2e9]
446 --stabilizeonly=bool
448 only stabilizing phases [false]
449 --stabilizephase=bool
451 use target variable phase [true]
452 --subsume=bool
454 enable clause subsumption [true]
455 --subsumebinlim=0..2e9
457 watch list length limit [1e4]
458 --subsumeclslim=0..2e9
460 clause length limit [1e3]
461 --subsumeint=1..2e9
463 subsume interval [1e4]
464 --subsumelimited=bool
466 limit subsumption checks [true]
467 --subsumemaxeff=0..2e9
469 maximum subsuming efficiency [1e8]
470 --subsumemineff=0..2e9
472 minimum subsuming efficiency [1e6]
473 --subsumeocclim=0..2e9
475 watch list length limit [1e2]
476 --subsumereleff=1..1e5
478 relative efficiency per mille [1e3]
479 --subsumestr=bool
481 strengthen during subsume [true]
482 --ternary=bool
484 hyper ternary resolution [true]
485 --ternarymaxadd=0..1e4
487 maximum clauses added in percent [1e3]
488 --ternarymaxeff=0..2e9
490 ternary maximum efficiency [1e8]
491 --ternarymineff=1..2e9
493 minimum ternary efficiency [1e6]
494 --ternaryocclim=1..2e9
496 ternary occurrence limit [1e2]
497 --ternaryreleff=1..1e5
499 relative efficiency in per mille [10]
500 --ternaryrounds=1..16
502 maximum ternary rounds [2]
503 --transred=bool
505 transitive reduction of BIG [true]
506 --transredmaxeff=0..2e9
508 maximum efficiency [1e8]
509 --transredmineff=0..2e9
511 minimum efficiency [1e6]
512 --transredreleff=1..1e5
514 relative efficiency per mille [1e2]
515 --verbose=0..3
517 more verbose messages [0]
518 --vivify=bool
520 vivification [true]
521 --vivifymaxeff=0..2e9
523 maximum efficiency [1e8]
524 --vivifymineff=0..2e9
526 minimum efficiency [1e5]
527 --vivifyonce=0..2
529 vivify once: 1=red, 2=red+irr [0]
530 --vivifyredeff=0..1e3
532 redundant efficiency per mille [300]
533 --vivifyreleff=1..1e5
535 relative efficiency per mille [80]
536 --walk=bool
538 enable random walks [true]
539 --walkmaxeff=0..2e9
541 maximum efficiency [1e7]
542 --walkmineff=0..1e7
544 minimum efficiency [1e5]
545 --walknonstable=bool
547 walk in non-stabilizing phase [true]
548 --walkredundant=bool
550 walk redundant clauses too [false]
551 --walkreleff=1..1e5
553 relative efficiency per mille [20]
554 The internal options have their default value printed in brackets after
556 their description. They can also be used in the form '--<name>' which
557 is equivalent to '--<name>=1' and in the form '--no-<name>' which is
558 equivalent to '--<name>=0'. One can also use 'true' instead of '1',
559 'false' instead of '0', as well as numbers with positive exponent such
560 as '1e3' instead of '1000'.
561 Alternatively option values can also be specified in the header of the
563 DIMACS file, e.g., 'c --elim=false', or through environment variables,
564 such as 'CADICAL_ELIM=false'. The embedded options in the DIMACS file
565 have highest priority, followed by command line options and then values
566 specified through environment variables.
567 There are also the following pre-defined configurations of options
569 --sat target satisfiable instances
571 --unsat
573 target unsatisfiable instances
574 The input is read from '<dimacs>' assumed to be in DIMACS format. If
576 '<proof>' is given then a DRAT proof is written to that file.
577 If '<dimacs>' is missing then the solver reads from '<stdin>', also if
579 '-' is used as input path name '<dimacs>'. Similarly, if '-' is speci‐
580 fied as '<proof>' path then a proof is generated and printed to '<std‐
581 out>'.
582 By default the proof is stored in the binary DRAT format unless the
584 option '--no-binary' is specified or the proof is written to '<std‐
585 out>' and '<stdout>' is connected to a terminal.
586 The input is assumed to be compressed if it is given explicitly and has
588 a '.gz', '.bz2', '.xz' or '.7z' suffix. The same applies to the output
589 file. In order to use compression and decompression the corresponding
590 utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are
591 required and need to be installed on the system.
592cadical 1.2.1 January 2020 CADICAL(1)