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]

       --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]

       --lucky=bool
              search for lucky phases [true]

       --minimize=bool
              minimize learned clauses [true]

       --minimizedepth=0..1e3
              minimization depth [1e3]

       --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]

       --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]

       --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.