--- name: "cadical" section: "1" platform: "linux" package: "cadical" version: "1.7.4-1+b1" release: "Debian 13 (Trixie)" platforms: ["linux"] url: "https://new.carta.tech/cadical" --- # cadical(1) CaDiCaL Simplified Satisfiability Solver ## NAME cadical - CaDiCaL Simplified Satisfiability Solver ## DESCRIPTION usage: cadical \[ \ ... \] \[ \ \[ \ \] \] where '\' is one of the following common options: - **-h** print alternatively only a list of common options - **--help** print this complete list of all options - **--version** print version - **-n** do not print witness (same as '--no-witness') - **-v** increase verbosity (see also '--verbose' below) - **-q** be quiet (same as '--quiet') - **-t** \ set wall clock time limit Or '\' is one of the less common options - **-L**\ run local search initially (default '0' rounds) - **-O**\ increase limits by '2^\' or '10^\' - **-P**\ initial preprocessing (default '0' rounds) Note there is no separating space for the options above while the following options require a space after the option name: - **-c** \ limit the number of conflicts (default unlimited) - **-d** \ limit the number of decisions (default unlimited) - **-o** \ write simplified CNF in DIMACS format to file - **-e** \ write reconstruction/extension stack to file - **--force** \| **-f** parsing broken DIMACS header and writing proofs - **--strict** strict parsing (no white space in header) - **-r** \ read solution in competition output format to check consistency of learned clauses during testing and debugging - **-w** \ write result including a potential witness solution in competition format to the given file - **--colors** force colored output - **--no-colors** disable colored output to terminal - **--no-witness** do not print witness (see also '-n' above) - **--build** print build configuration - **--copyright** print copyright information There are pre-defined configurations of advanced internal options: - **--default** set default advanced internal options - **--plain** disable all internal preprocessing options - **--sat** set internal options to target satisfiable instances - **--unsat** set internal options to target unsatisfiable instances Or '\' is one of the following advanced internal options: - **--arena**=*bool* allocate clauses in arena \[true\] - **--arenacompact**=*bool* keep clauses compact \[true\] - **--arenasort**=*bool* sort clauses in arena \[true\] - **--arenatype**=*1*..3 1=clause, 2=var, 3=queue \[3\] - **--binary**=*bool* use binary proof format \[true\] - **--block**=*bool* blocked clause elimination \[false\] - **--blockmaxclslim**=*1*..2e9 maximum clause size \[1e5\] - **--blockminclslim**=*2*..2e9 minimum clause size \[2\] - **--blockocclim**=*1*..2e9 occurrence limit \[1e2\] - **--bump**=*bool* bump variables \[true\] - **--bumpreason**=*bool* bump reason literals too \[true\] - **--bumpreasondepth**=*1*..3 bump reason depth \[1\] - **--check**=*bool* enable internal checking \[false\] - **--checkassumptions**=*bool* check assumptions satisfied \[true\] - **--checkconstraint**=*bool* check constraint satisfied \[true\] - **--checkfailed**=*bool* check failed literals form core \[true\] - **--checkfrozen**=*bool* check all frozen semantics \[false\] - **--checkproof**=*bool* check proof internally \[true\] - **--checkprooflrat**=*bool* use internal LRAT proof checker \[true\] - **--checkwitness**=*bool* check witness internally \[true\] - **--chrono**=*0*..2 chronological backtracking \[1\] - **--chronoalways**=*bool* force always chronological \[false\] - **--chronolevelim**=*0*..2e9 chronological level limit \[1e2\] - **--chronoreusetrail**=*bool* reuse trail chronologically \[true\] - **--compact**=*bool* compact internal variables \[true\] - **--compactint**=*1*..2e9 compacting interval \[2e3\] - **--compactlim**=*0*..1e3 inactive limit per mille \[1e2\] - **--compactmin**=*1*..2e9 minimum inactive limit \[1e2\] - **--condition**=*bool* globally blocked clause elim \[false\] - **--conditionint**=*1*..2e9 initial conflict interval \[1e4\] - **--conditionmaxeff**=*0*..2e9 maximum condition efficiency \[1e7\] - **--conditionmaxrat**=*1*..2e9 maximum clause variable ratio \[100\] - **--conditionmineff**=*0*..2e9 minimum condition efficiency \[1e6\] - **--conditionreleff**=*1*..1e5 relative efficiency per mille \[100\] - **--cover**=*bool* covered clause elimination \[false\] - **--covermaxclslim**=*1*..2e9 maximum clause size \[1e5\] - **--covermaxeff**=*0*..2e9 maximum cover efficiency \[1e8\] - **--coverminclslim**=*2*..2e9 minimum clause size \[2\] - **--covermineff**=*0*..2e9 minimum cover efficiency \[1e6\] - **--coverreleff**=*1*..1e5 relative efficiency per mille \[4\] - **--decompose**=*bool* decompose BIG in SCCs and ELS \[true\] - **--decomposerounds**=*1*..16 number of decompose rounds \[2\] - **--deduplicate**=*bool* remove duplicated binaries \[true\] - **--eagersubsume**=*bool* subsume recently learned \[true\] - **--eagersubsumelim**=*1*..1e3 limit on subsumed candidates \[20\] - **--elim**=*bool* bounded variable elimination \[true\] - **--elimands**=*bool* find AND gates \[true\] - **--elimaxeff**=*0*..2e9 maximum elimination efficiency \[2e9\] - **--elimbackward**=*bool* eager backward subsumption \[true\] - **--elimboundmax**=*-1*..2e6 maximum elimination bound \[16\] - **--elimboundmin**=*-1*..2e6 minimum elimination bound \[0\] - **--elimclslim**=*2*..2e9 resolvent size limit \[1e2\] - **--elimequivs**=*bool* find equivalence gates \[true\] - **--elimineff**=*0*..2e9 minimum elimination efficiency \[1e7\] - **--elimint**=*1*..2e9 elimination interval \[2e3\] - **--elimites**=*bool* find if-then-else gates \[true\] - **--elimlimited**=*bool* limit resolutions \[true\] - **--elimocclim**=*0*..2e9 occurrence limit \[1e2\] - **--elimprod**=*0*..1e4 elim score product weight \[1\] - **--elimreleff**=*1*..1e5 relative efficiency per mille \[1e3\] - **--elimrounds**=*1*..512 usual number of rounds \[2\] - **--elimsubst**=*bool* elimination by substitution \[true\] - **--elimsum**=*0*..1e4 elimination score sum weight \[1\] - **--elimxorlim**=*2*..27 maximum XOR size \[5\] - **--elimxors**=*bool* find XOR gates \[true\] - **--emagluefast**=*1*..2e9 window fast glue \[33\] - **--emaglueslow**=*1*..2e9 window slow glue \[1e5\] - **--emajump**=*1*..2e9 window back-jump level \[1e5\] - **--emalevel**=*1*..2e9 window back-track level \[1e5\] - **--emasize**=*1*..2e9 window learned clause size \[1e5\] - **--ematrailfast**=*1*..2e9 window fast trail \[1e2\] - **--ematrailslow**=*1*..2e9 window slow trail \[1e5\] - **--flush**=*bool* flush redundant clauses \[false\] - **--flushfactor**=*1*..1e3 interval increase \[3\] - **--flushint**=*1*..2e9 initial limit \[1e5\] - **--forcephase**=*bool* always use initial phase \[false\] - **--inprocessing**=*bool* enable inprocessing \[true\] - **--instantiate**=*bool* variable instantiation \[false\] **--instantiateclslim**=*2*..2e9 minimum clause size \[3\] **--instantiateocclim**=*1*..2e9 maximum occurrence limit \[1\] - **--instantiateonce**=*bool* instantiate each clause once \[true\] - **--lrat**=*bool* use lrat proof format \[false\] - **--lratexternal**=*bool* external lrat \[false\] - **--lratfrat**=*bool* use frat proof format \[false\] - **--lratveripb**=*bool* veriPB proofs. needs lrat=1 \[false\] - **--lucky**=*bool* search for lucky phases \[true\] - **--minimize**=*bool* minimize learned clauses \[true\] - **--minimizedepth**=*0*..1e3 minimization depth \[1e3\] - **--otfs**=*bool* on-the-fly self subsumption \[true\] - **--phase**=*bool* initial phase \[true\] - **--probe**=*bool* failed literal probing \[true\] - **--probehbr**=*bool* learn hyper binary clauses \[true\] - **--probeint**=*1*..2e9 probing interval \[5e3\] - **--probemaxeff**=*0*..2e9 maximum probing efficiency \[1e8\] - **--probemineff**=*0*..2e9 minimum probing efficiency \[1e6\] - **--probereleff**=*1*..1e5 relative efficiency per mille \[20\] - **--proberounds**=*1*..16 probing rounds \[1\] - **--profile**=*0*..4 profiling level \[2\] - **--quiet**=*bool* disable all messages \[false\] - **--radixsortlim**=*0*..2e9 radix sort limit \[800\] - **--realtime**=*bool* real instead of process time \[false\] - **--reduce**=*bool* reduce useless clauses \[true\] - **--reduceint**=*10*..1e6 reduce interval \[300\] - **--reducetarget**=*10*..1e2 reduce fraction in percent \[75\] - **--reducetier1glue**=*1*..2e9 glue of kept learned clauses \[2\] - **--reducetier2glue**=*1*..2e9 glue of tier two clauses \[6\] - **--reluctant**=*0*..2e9 reluctant doubling period \[1024\] - **--reluctantmax**=*0*..2e9 reluctant doubling period \[1048576\] - **--rephase**=*bool* enable resetting phase \[true\] - **--rephaseint**=*1*..2e9 rephase interval \[1e3\] - **--report**=*bool* enable reporting \[false\] - **--reportall**=*bool* report even if not successful \[false\] - **--reportsolve**=*bool* use solving not process time \[false\] - **--restart**=*bool* enable restarts \[true\] - **--restartint**=*1*..2e9 restart interval \[2\] - **--restartmargin**=*0*..1e2 slow fast margin in percent \[10\] - **--restartreusetrail**=*bool* enable trail reuse \[true\] - **--restoreall**=*0*..2 restore all clauses (2=really) \[0\] - **--restoreflush**=*bool* remove satisfied clauses \[false\] - **--reverse**=*bool* reverse variable ordering \[false\] - **--score**=*bool* use EVSIDS scores \[true\] - **--scorefactor**=*500*..1e3 score factor per mille \[950\] - **--seed**=*0*..2e9 random seed \[0\] - **--shrink**=*0*..3 shrink conflict clause \[3\] - **--shrinkreap**=*bool* use a reap for shrinking \[true\] - **--shuffle**=*bool* shuffle variables \[false\] - **--shufflequeue**=*bool* shuffle variable queue \[true\] - **--shufflerandom**=*bool* not reverse but random \[false\] - **--shufflescores**=*bool* shuffle variable scores \[true\] - **--stabilize**=*bool* enable stabilizing phases \[true\] **--stabilizefactor**=*101*..2e9 phase increase in percent \[200\] - **--stabilizeint**=*1*..2e9 stabilizing interval \[1e3\] - **--stabilizemaxint**=*1*..2e9 maximum stabilizing phase \[2e9\] - **--stabilizeonly**=*bool* only stabilizing phases \[false\] - **--stats**=*bool* print all statistics at the end of the run \[true\] - **--subsume**=*bool* enable clause subsumption \[true\] - **--subsumebinlim**=*0*..2e9 watch list length limit \[1e4\] - **--subsumeclslim**=*0*..2e9 clause length limit \[1e2\] - **--subsumeint**=*1*..2e9 subsume interval \[1e4\] - **--subsumelimited**=*bool* limit subsumption checks \[true\] - **--subsumemaxeff**=*0*..2e9 maximum subsuming efficiency \[1e8\] - **--subsumemineff**=*0*..2e9 minimum subsuming efficiency \[1e6\] - **--subsumeocclim**=*0*..2e9 watch list length limit \[1e2\] - **--subsumereleff**=*1*..1e5 relative efficiency per mille \[1e3\] - **--subsumestr**=*bool* strengthen during subsume \[true\] - **--target**=*0*..2 target phases (1=stable only) \[1\] - **--terminateint**=*0*..1e4 termination check interval \[10\] - **--ternary**=*bool* hyper ternary resolution \[true\] - **--ternarymaxadd**=*0*..1e4 max clauses added in percent \[1e3\] - **--ternarymaxeff**=*0*..2e9 ternary maximum efficiency \[1e8\] - **--ternarymineff**=*1*..2e9 minimum ternary efficiency \[1e6\] - **--ternaryocclim**=*1*..2e9 ternary occurrence limit \[1e2\] - **--ternaryreleff**=*1*..1e5 relative efficiency per mille \[10\] - **--ternaryrounds**=*1*..16 maximum ternary rounds \[2\] - **--transred**=*bool* transitive reduction of BIG \[true\] - **--transredmaxeff**=*0*..2e9 maximum efficiency \[1e8\] - **--transredmineff**=*0*..2e9 minimum efficiency \[1e6\] - **--transredreleff**=*1*..1e5 relative efficiency per mille \[1e2\] - **--verbose**=*0*..3 more verbose messages \[0\] - **--vivify**=*bool* vivification \[true\] - **--vivifyinst**=*bool* instantiate last literal when vivify \[true\] - **--vivifymaxeff**=*0*..2e9 maximum efficiency \[2e7\] - **--vivifymineff**=*0*..2e9 minimum efficiency \[2e4\] - **--vivifyonce**=*0*..2 vivify once: 1=red, 2=red+irr \[0\] - **--vivifyredeff**=*0*..1e3 redundant efficiency per mille \[75\] - **--vivifyreleff**=*1*..1e5 relative efficiency per mille \[20\] - **--walk**=*bool* enable random walks \[true\] - **--walkmaxeff**=*0*..2e9 maximum efficiency \[1e7\] - **--walkmineff**=*0*..1e7 minimum efficiency \[1e5\] - **--walknonstable**=*bool* walk in non-stabilizing phase \[true\] - **--walkredundant**=*bool* walk redundant clauses too \[false\] - **--walkreleff**=*1*..1e5 relative efficiency per mille \[20\] The internal options have their default value printed in brackets after their description. They can also be used in the form '--\' which is equivalent to '--\=1' and in the form '--no-\' which is equivalent to '--\=0'. One can also use 'true' instead of '1', 'false' instead of '0', as well as numbers with positive exponent such as '1e3' instead of '1000'. Alternatively option values can also be specified in the header of the DIMACS file, e.g., 'c **--elim**=*false*', or through environment variables, such as 'CADICAL\_ELIM=false'. The embedded options in the DIMACS file have highest priority, followed by command line options and then values specified through environment variables. The input is read from '\' assumed to be in DIMACS format. Incremental 'p inccnf' files are supported too with cubes at the end. If '\' is given then a DRAT proof is written to that file. If '\' is missing then the solver reads from '\', also if '-' is used as input path name '\'. Similarly, For incremental files each cube is solved in turn. The solver stops at the first satisfied cube if there is one and uses that one for the witness to print. Conflict and decision limits are applied to each individual cube solving call while '-P', '-L' and '-t' remain global. Only if all cubes were unsatisfiable the solver prints the standard unsatisfiable solution line ('s UNSATISFIABLE'). By default the proof is stored in the binary DRAT format unless the option '--no-binary' is specified or the proof is written to '\' and '\' is connected to a terminal. The input is assumed to be compressed if it is given explicitly and has a '.gz', '.bz2', '.xz' or '.7z' suffix. The same applies to the output file. In order to use compression and decompression the corresponding utilities 'gzip', 'bzip', 'xz', and '7z' (depending on the format) are required and need to be installed on the system. The solver checks file type signatures though and falls back to non-compressed file reading if the signature does not match.