/usr/bin/cadical

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]
  --backbone=0..2            binary clause backbone [1]
  --backboneeffort=0..1e5    binary effort in per mile [20]
  --backbonemaxrounds=0..1e5 backbone rounds limit [1e3]
  --backbonerounds=0..1e5    backbone rounds limit [100]
  --backbonethresh=0..1e9    delay if ticks smaller thresh*clauses [5]
  --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]
  --bumpreasonlimit=1..2e9   bump reason limit [10]
  --bumpreasonrate=1..2e9    bump reason decision rate [100]
  --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=0..3          1=drat, 2=lrat, 3=both [3]
  --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]
  --conditioneffort=1..1e5   relative efficiency per mille [100]
  --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 [0]
  --congruence=bool          congruence closure [true]
  --congruenceand=bool       extract AND gates [true]
  --congruenceandarity=2..5e7 AND gate arity limit [1e6]
  --congruencebinaries=bool  extract binary and strengthen ternary clauses [true]
  --congruenceite=bool       extract ITE gates [true]
  --congruencexor=bool       extract XOR gates [true]
  --congruencexorarity=2..31 XOR gate arity limit [4]
  --congruencexorcounts=1..5e6 XOR gate round [1]
  --cover=bool               covered clause elimination [false]
  --covereffort=1..1e5       relative efficiency per mille [4]
  --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 [0]
  --decompose=bool           decompose BIG in SCCs and ELS [true]
  --decomposerounds=1..16    number of decompose rounds [2]
  --deduplicate=bool         remove duplicated binaries [true]
  --deduplicateallinit=bool  remove duplicated clauses once before solving [false]
  --eagersubsume=bool        subsume recently learned [true]
  --eagersubsumelim=1..1e3   limit on subsumed candidates [20]
  --elevate=-1..3            elevate during clause addition [2]
  --elim=bool                bounded variable elimination [true]
  --elimands=bool            find AND gates [true]
  --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]
  --elimdef=bool             mine definitions with kitten [false]
  --elimdefcores=1..100      number of unsat cores [1]
  --elimdefticks=0..2e9      kitten ticks limit [2e5]
  --elimeffort=1..1e5        relative efficiency per mille [1e3]
  --elimequivs=bool          find equivalence gates [true]
  --elimint=1..2e9           elimination interval [2e3]
  --elimites=bool            find if-then-else gates [true]
  --elimlimited=bool         limit resolutions [true]
  --elimmaxeff=0..2e9        maximum elimination efficiency [2e9]
  --elimmineff=0..2e9        minimum elimination efficiency [1e7]
  --elimocclim=0..2e9        occurrence limit [1e2]
  --elimprod=0..1e4          elim score product weight [1]
  --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]
  --emadecisions=1..2e9      window decision rate [1e5]
  --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]
  --exteagerreasons=bool     eagerly ask for all reasons (0: only when needed) [false]
  --exteagerrecalc=bool      after eagerly asking for reasons recalculate all levels (0: trust the external tool) [true]
  --exttracecalls=bool       trace propagator call-backs when tracing API calls [false]
  --factor=bool              bounded variable addition [false]
  --factorcandrounds=0..2e9  candidates reduction rounds [2]
  --factorcheck=0..2         API checks that variables have been declared (1 = only with factor on, 2 = always) [1]
  --factordelay=0..12        delay bounded variable addition between eliminations [4]
  --factoreffort=0..1e6      relative effort per mille [50]
  --factoriniticks=1..1e6    initial effort in millions [300]
  --factorsize=2..2e9        clause size limit [5]
  --factorthresh=0..100      delay if ticks smaller thresh*clauses [7]
  --factorunbump=bool        extension variable with lowest importance [1: as in kissat] [true]
  --fastelim=bool            fast BVE during preprocessing [true]
  --fastelimbound=1..1e3     fast BVE bound during preprocessing [8]
  --fastelimclslim=2..2e9    fast BVE resolvent size limit [1e2]
  --fastelimocclim=1..2e9    fast BVE occurence limit during preprocessing [100]
  --fastelimrounds=1..512    number of fastelim rounds [4]
  --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]
  --frat=0..2                1=frat(lrat), 2=frat(drat) [0]
  --idrup=bool               incremental proof format [false]
  --ilb=0..2                 ILB (incremental lazy backtrack) (0: no, 1: assumptions only, 2: everything) [0]
  --incdecay=0..4            decay clauses when doing incremental clauses [1]
  --incdecayint=1..2e9       decay interval when doing incremental clauses [1e6]
  --inprobeint=1..2e9        inprobing interval [100]
  --inprobing=bool           enable probe inprocessing [true]
  --inprocessing=bool        enable general 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]
  --lidrup=bool              linear incremental proof format [false]
  --lrat=bool                use LRAT proof format [false]
  --lucky=bool               lucky phases [true]
  --luckyassumptions=bool    lucky phases with assumptions [true]
  --luckyearly=bool          lucky phases before preprocessing [true]
  --luckylate=bool           lucky phases after preprocessing [true]
  --minimize=bool            minimize learned clauses [true]
  --minimizedepth=0..1e3     minimization depth [1e3]
  --minimizeticks=bool       increment ticks in minimization [true]
  --otfs=bool                on-the-fly self subsumption [true]
  --phase=bool               initial phase [true]
  --preprocessinit=0..2e9    initial preprocessing base limit [2e6]
  --preprocesslight=bool     lightweight preprocessing [false]
  --probe=bool               failed literal probing [true]
  --probeeffort=1..1e5       relative efficiency per mille [8]
  --probehbr=bool            learn hyper binary clauses [true]
  --probethresh=0..100       delay if ticks smaller thresh*clauses [0]
  --profile=0..4             profiling level [2]
  --quiet=bool               disable all messages [false]
  --radixsortlim=0..2e9      radix sort limit [32]
  --randec=bool              random decisions [false]
  --randecfocused=bool       random decisions in focused mode [true]
  --randecinit=2..2e9        inital random decision interval [1e3]
  --randecint=0..2e9         random conflict length [500]
  --randeclength=1..1e9      length random decisions phases [10]
  --randecstable=bool        random decisions in stable mode [false]
  --realtime=bool            real instead of process time [false]
  --recomputetier=bool       recompute tiers [true]
  --reduce=bool              reduce useless clauses [true]
  --reduceinit=1..1e6        initial interval [300]
  --reduceint=2..1e6         reduce interval [25]
  --reduceopt=0..2           0=prct,1=sqrt,2=max [1]
  --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=bool           stable reluctant doubling restarts [true]
  --reluctantint=0..2e9      reluctant doubling period [1024]
  --reluctantmax=0..2e9      maximum reluctant doubling period [1048576]
  --rephase=0..2             enable resetting phase (0=no,1=always,2=stable-only) [1]
  --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]
  --restartmarginfocused=0..25 focused slow fast margin in percent [10]
  --restartmarginstable=0..25 stable slow fast margin in percent [25]
  --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 (1=binary-only,2=minimize-on-pulling,3=full) [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]
  --stabilizeinit=1..2e9     stabilizing interval [1e3]
  --stabilizeonly=bool       only stabilizing phases [false]
  --stats=bool               print all statistics at the end of the run [false]
  --stubbornIOfocused=bool   force phases to I/O in focused mode every once in a while (requires rephase==2) [false]
  --subsume=bool             enable clause subsumption [true]
  --subsumebinlim=0..2e9     watch list length limit [1e4]
  --subsumeclslim=0..2e9     clause length limit [1e2]
  --subsumeeffort=1..1e5     relative efficiency per mille [1e3]
  --subsumelimited=bool      limit subsumption checks [true]
  --subsumemaxeff=0..2e9     maximum subsuming efficiency [1e8]
  --subsumemineff=0..2e9     minimum subsuming efficiency [0]
  --subsumeocclim=0..2e9     watch list length limit [1e2]
  --subsumestr=bool          subsume strengthen [true]
  --sweep=bool               enable SAT sweeping [true]
  --sweepclauses=0..2e9      environment clauses [1024]
  --sweepcomplete=bool       run SAT sweeping to completion [false]
  --sweepcountbinary=bool    count binaries to environment [true]
  --sweepdepth=0..2e9        environment depth [2]
  --sweepeffort=0..1e4       relative effort in ticks per mille [1e2]
  --sweepfliprounds=0..2e9   flipping rounds [1]
  --sweepmaxclauses=2..2e9   maximum environment clauses [3e5]
  --sweepmaxdepth=1..2e9     maximum environment depth [3]
  --sweepmaxvars=2..2e9      maximum environment variables [8192]
  --sweeprand=bool           randomize sweeping environment [false]
  --sweepthresh=0..100       delay if ticks smaller thresh*clauses [5]
  --sweepvars=0..2e9         environment variables [256]
  --target=0..2              target phases (1=stable only) [1]
  --terminateint=0..1e4      termination check interval [10]
  --ternary=bool             hyper ternary resolution [true]
  --ternaryeffort=1..1e5     relative efficiency per mille [8]
  --ternarymaxadd=0..1e4     max clauses added in percent [1e3]
  --ternaryocclim=1..2e9     ternary occurrence limit [1e2]
  --ternaryrounds=1..16      maximum ternary rounds [2]
  --ternarythresh=0..100     delay if ticks smaller thresh*clauses [6]
  --tier1limit=0..100        limit of tier1 usage in percentage [50]
  --tier1minglue=0..100      lowest tier1 limit [0]
  --tier2limit=0..100        limit of tier2 usage in percentage [90]
  --tier2minglue=0..100      lowest tier2 limit [0]
  --transred=bool            transitive reduction of BIG [true]
  --transredeffort=1..1e5    relative efficiency per mille [1e2]
  --transredmaxeff=0..2e9    maximum efficiency [1e8]
  --transredmineff=0..2e9    minimum efficiency [0]
  --verbose=0..3             more verbose messages [0]
  --veripb=0..4              odd=check-deletions, >2 drat [0]
  --vivify=bool              vivification [true]
  --vivifycalctier=bool      recalculate tier limits [false]
  --vivifydemote=bool        demote irredundant or delete directly [false]
  --vivifyeffort=0..1e5      overall efficiency per mille [50]
  --vivifyflush=bool         flush subsumed before vivification rounds [true]
  --vivifyinst=bool          instantiate last literal when vivify [true]
  --vivifyirred=bool         vivification of irredundant clauses [true]
  --vivifyirredeff=1..100    irredundant efficiency per mille [3]
  --vivifyonce=0..2          vivify once: 1=red, 2=red+irr [0]
  --vivifyretry=0..5         re-vivify clause if vivify was successful [0]
  --vivifyschedmax=10..2e9   maximum schedule size [5e3]
  --vivifythresh=0..100      delay if ticks smaller thresh*clauses [20]
  --vivifytier1=bool         vivification tier1 [true]
  --vivifytier1eff=0..100    relative tier1 effort [4]
  --vivifytier2=bool         vivification tier2 [true]
  --vivifytier2eff=1..100    relative tier2 effort [2]
  --vivifytier3=bool         vivification tier3 [true]
  --vivifytier3eff=1..100    relative tier3 effort [1]
  --walk=bool                enable random walks [true]
  --walkeffort=1..1e5        relative efficiency per mille [80]
  --walkfullocc=bool         use Kissat's full occurrences instead of the single watched [false]
  --walkmaxeff=0..2e9        maximum efficiency (in 1e3 ticks) [1e7]
  --walkmineff=0..1e7        minimum efficiency [0]
  --walknonstable=bool       walk in non-stabilizing phase [true]
  --walkredundant=bool       walk redundant clauses too [false]
  --warmup=bool              warmup before walk using propagation [true]

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.