Provided by: cadical_1.7.4-1_amd64 
NAME
cadical - CaDiCaL Simplified Satisfiability Solver
DESCRIPTION
usage: cadical [ <option> ... ] [ <input> [ <proof> ] ]
where '<option>' 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 <sec>
set wall clock time limit
Or '<option>' is one of the less common options
-L<rounds>
run local search initially (default '0' rounds)
-O<level>
increase limits by '2^<level>' or '10^<level>'
-P<rounds>
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>
limit the number of conflicts (default unlimited)
-d <limit>
limit the number of decisions (default unlimited)
-o <output>
write simplified CNF in DIMACS format to file
-e <extend>
write reconstruction/extension stack to file
--force | -f
parsing broken DIMACS header and writing proofs
--strict
strict parsing (no white space in header)
-r <sol>
read solution in competition output format to check consistency of learned clauses during testing
and debugging
-w <sol>
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 '<option>' 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 '--<name>' which is equivalent to '--<name>=1' and in the form '--no-<name>' which is
equivalent to '--<name>=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 '<input>' assumed to be in DIMACS format. Incremental 'p inccnf' files are
supported too with cubes at the end. If '<proof>' is given then a DRAT proof is written to that file.
If '<input>' is missing then the solver reads from '<stdin>', also if '-' is used as input path name
'<input>'. 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 '<stdout>' and '<stdout>' 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.
cadical 1.7.4 February 2024 CADICAL(1)