.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.49.3.
.TH CRYPTOMINISAT5 "1" "May 2024" "cryptominisat5 5.11.21" "User Commands"
.SH NAME
cryptominisat5 \- manual page for cryptominisat5 5.11.21
.SH SYNOPSIS
.B cryptominisat5
[\fI\,--help\/\fR] [\fI\,--version\/\fR] [\fI\,--help VAR\/\fR] [\fI\,--version\/\fR] [\fI\,--verb VAR\/\fR] [\fI\,--maxtime VAR\/\fR] [\fI\,--maxconfl VAR\/\fR] [\fI\,--random VAR\/\fR] [\fI\,--threads VAR\/\fR] [\fI\,--mult VAR\/\fR] [\fI\,--nextm VAR\/\fR] [\fI\,--memoutmult VAR\/\fR] [\fI\,--maxsol VAR\/\fR] [\fI\,--polar VAR\/\fR] [\fI\,--scc VAR\/\fR] [\fI\,--restart VAR\/\fR] [\fI\,--rstfirst VAR\/\fR] [\fI\,--gluehist VAR\/\fR] [\fI\,--lwrbndblkrest VAR\/\fR] [\fI\,--locgmult VAR\/\fR] [\fI\,--ratiogluegeom VAR\/\fR] [\fI\,--blockingglue VAR\/\fR] [\fI\,--gluecut0 VAR\/\fR] [\fI\,--gluecut1 VAR\/\fR] [\fI\,--adjustglue VAR\/\fR] [\fI\,--everylev1 VAR\/\fR] [\fI\,--everylev2 VAR\/\fR] [\fI\,--lev1usewithin VAR\/\fR] [\fI\,--branchstr VAR\/\fR] [\fI\,--nobansol\/\fR] [\fI\,--debuglib VAR\/\fR] [\fI\,--breakid VAR\/\fR] [\fI\,--breakideveryn VAR\/\fR] [\fI\,--breakidmaxlits VAR\/\fR] [\fI\,--breakidmaxcls VAR\/\fR] [\fI\,--breakidmaxvars VAR\/\fR] [\fI\,--breakidtime VAR\/\fR] [\fI\,--breakidcls VAR\/\fR] [\fI\,--breakidmatrix VAR\/\fR] [\fI\,--sls VAR\/\fR] [\fI\,--slstype VAR\/\fR] [\fI\,--slsmaxmem VAR\/\fR] [\fI\,--slseveryn VAR\/\fR] [\fI\,--yalsatmems VAR\/\fR] [\fI\,--walksatruns VAR\/\fR] [\fI\,--slsgetphase VAR\/\fR] [\fI\,--slsccnraspire VAR\/\fR] [\fI\,--slstobump VAR\/\fR] [\fI\,--slstobumpmaxpervar VAR\/\fR] [\fI\,--slsbumptype VAR\/\fR] [\fI\,--transred VAR\/\fR] [\fI\,--intree VAR\/\fR] [\fI\,--intreemaxm VAR\/\fR] [\fI\,--otfhyper VAR\/\fR] [\fI\,--schedsimp VAR\/\fR] [\fI\,--presimp VAR\/\fR] [\fI\,--allpresimp VAR\/\fR] [\fI\,--nonstop VAR\/\fR] [\fI\,--maxnumsimppersolve VAR\/\fR] [\fI\,--schedule VAR\/\fR] [\fI\,--preschedule VAR\/\fR] [\fI\,--occsimp VAR\/\fR] [\fI\,--confbtwsimp VAR\/\fR] [\fI\,--confbtwsimpinc VAR\/\fR] [\fI\,--tern VAR\/\fR] [\fI\,--terntimelim VAR\/\fR] [\fI\,--ternkeep VAR\/\fR] [\fI\,--terncreate VAR\/\fR] [\fI\,--ternbincreate VAR\/\fR] [\fI\,--occredmax VAR\/\fR] [\fI\,--occredmaxmb VAR\/\fR] [\fI\,--occirredmaxmb VAR\/\fR] [\fI\,--strengthen VAR\/\fR] [\fI\,--weakentimelim VAR\/\fR] [\fI\,--substimelim VAR\/\fR] [\fI\,--substimelimbinratio VAR\/\fR] [\fI\,--substimelimlongratio VAR\/\fR] [\fI\,--strstimelim VAR\/\fR] [\fI\,--sublonggothrough VAR\/\fR] [\fI\,--bva VAR\/\fR] [\fI\,--bvaeveryn VAR\/\fR] [\fI\,--bvalim VAR\/\fR] [\fI\,--bva2lit VAR\/\fR] [\fI\,--bvato VAR\/\fR] [\fI\,--varelim VAR\/\fR] [\fI\,--varelimto VAR\/\fR] [\fI\,--varelimover VAR\/\fR] [\fI\,--emptyelim VAR\/\fR] [\fI\,--varelimmaxmb VAR\/\fR] [\fI\,--eratio VAR\/\fR] [\fI\,--varelimcheckres VAR\/\fR] [\fI\,--xor VAR\/\fR] [\fI\,--maxxorsize VAR\/\fR] [\fI\,--xorfindtout VAR\/\fR] [\fI\,--varsperxorcut VAR\/\fR] [\fI\,--maxxormat VAR\/\fR] [\fI\,--forcepreservexors VAR\/\fR] [\fI\,--gates VAR\/\fR] [\fI\,--printgatedot VAR\/\fR] [\fI\,--gatefindto VAR\/\fR] [\fI\,--recur VAR\/\fR] [\fI\,--moreminim VAR\/\fR] [\fI\,--moremoreminim VAR\/\fR] [\fI\,--moremorealways VAR\/\fR] [\fI\,--decbased VAR\/\fR] [\fI\,--updateglueonanalysis VAR\/\fR] [\fI\,--maxgluehistltlimited VAR\/\fR] [\fI\,--diffdeclevelchrono VAR\/\fR] [\fI\,--verbstat VAR\/\fR] [\fI\,--verbrestart VAR\/\fR] [\fI\,--verballrestarts VAR\/\fR] [\fI\,--printsol,s VAR\/\fR] [\fI\,--restartprint VAR\/\fR] [\fI\,--distill VAR\/\fR] [\fI\,--distillbin VAR\/\fR] [\fI\,--distillmaxm VAR\/\fR] [\fI\,--distillincconf VAR\/\fR] [\fI\,--distillminconf VAR\/\fR] [\fI\,--distilltier0ratio VAR\/\fR] [\fI\,--distilltier1ratio VAR\/\fR] [\fI\,--distillirredalsoremratio VAR\/\fR] [\fI\,--distillirrednoremratio VAR\/\fR] [\fI\,--distillshuffleeveryn VAR\/\fR] [\fI\,--distillsort VAR\/\fR] [\fI\,--renumber VAR\/\fR] [\fI\,--mustconsolidate VAR\/\fR] [\fI\,--savemem VAR\/\fR] [\fI\,--mustrenumber VAR\/\fR] [\fI\,--fullwatchconseveryn VAR\/\fR] [\fI\,--strmaxt VAR\/\fR] [\fI\,--implicitmanip VAR\/\fR] [\fI\,--implsubsto VAR\/\fR] [\fI\,--implstrto VAR\/\fR] [\fI\,--cardfind VAR\/\fR] [\fI\,--sync VAR\/\fR] [\fI\,--clearinter VAR\/\fR] [\fI\,--zero-exit-status\/\fR] [\fI\,--printtimes VAR\/\fR] [\fI\,--maxsccdepth VAR\/\fR] [\fI\,--simfrat VAR\/\fR] [\fI\,--sampling VAR\/\fR] [\fI\,--onlysampling\/\fR] [\fI\,--assump VAR\/\fR] [\fI\,--maxmatrixrows VAR\/\fR] [\fI\,--maxmatrixcols VAR\/\fR] [\fI\,--autodisablegauss VAR\/\fR] [\fI\,--minmatrixrows VAR\/\fR] [\fI\,--maxnummatrices VAR\/\fR] [\fI\,--detachxor VAR\/\fR] [\fI\,--useallmatrixes VAR\/\fR] [\fI\,--detachverb VAR\/\fR] [\fI\,--gaussusefulcutoff VAR\/\fR] [\fI\,--dumpresult VAR\/\fR] \fI\,files\/\fR
.SH DESCRIPTION
A universal, fast SAT solver with XOR and Gaussian Elimination support.
Input can be either plain or gzipped DIMACS with XOR extension
.PP
cryptominisat5 [options] inputfile [frat\-file]
.SS "Positional arguments:"
.TP
files
input file and FRAT output [nargs: 0 or more]
.SS "Optional arguments:"
.TP
\fB\-h\fR, \fB\-\-help\fR
shows help message and exits
.TP
\fB\-v\fR, \fB\-\-version\fR
prints version information and exits
.TP
\fB\-h\fR, \fB\-\-help\fR
Print extensive help [nargs=0..1] [default: false]
.TP
\fB\-v\fR, \fB\-\-version\fR
Print version info
.TP
\fB\-\-verb\fR
[0\-10] Verbosity of solver. 0 = only solution [nargs=0..1] [default: 1]
.TP
\fB\-\-maxtime\fR
Stop solving after this much time (s)
.TP
\fB\-\-maxconfl\fR
Stop solving after this many conflicts
.TP
\fB\-r\fR, \fB\-\-random\fR
[0..] Random seed [nargs=0..1] [default: 0]
.TP
\fB\-t\fR, \fB\-\-threads\fR
Number of threads [nargs=0..1] [default: 1]
.TP
\fB\-m\fR, \fB\-\-mult\fR
Time multiplier for all simplification cutoffs [nargs=0..1] [default: 3]
.TP
\fB\-\-nextm\fR
Global multiplier when the next inprocessing should take place [nargs=0..1] [default: 1]
.TP
\fB\-\-memoutmult\fR
Multiplier for memory\-out checks on inprocessing functions. It limits things such as clause\-link\-in. Useful when you have limited memory but still want to do some inprocessing [nargs=0..1] [default: 1]
.TP
\fB\-\-maxsol\fR
Search for given amount of solutions. Thanks to Jannis Harder for the decision\-based banning idea [nargs=0..1] [default: 1]
.TP
\fB\-\-polar\fR
{true,false,rnd,auto,stable} Selects polarity mode. 'true' \-> selects only positive polarity when branching. 'false' \-> selects only negative polarity when branching. 'auto' \-> selects last polarity used (also called 'caching') [nargs=0..1] [default: "auto"]
.TP
\fB\-\-scc\fR
Find equivalent literals through SCC and replace them [nargs=0..1] [default: 1]
.TP
\fB\-\-restart\fR
{geom, glue, luby}  Restart strategy to follow. [nargs=0..1] [default: "auto"]
.TP
\fB\-\-rstfirst\fR
The size of the base restart [nargs=0..1] [default: 100]
.TP
\fB\-\-gluehist\fR
The size of the moving window for short\-term glue history of redundant clauses. If higher, the minimal number of conflicts between restarts is longer [nargs=0..1] [default: 50]
.TP
\fB\-\-lwrbndblkrest\fR
Lower bound on blocking restart \fB\-\-\fR don't block before this many conflicts [nargs=0..1] [default: 10000]
.TP
\fB\-\-locgmult\fR
The multiplier used to determine if we should restart during glue\-based restart [nargs=0..1] [default: 0.8]
.TP
\fB\-\-ratiogluegeom\fR
Ratio of glue vs geometric restarts \fB\-\-\fR more is more glue [nargs=0..1] [default: 5]
.TP
\fB\-\-blockingglue\fR
Do blocking restart for glues [nargs=0..1] [default: 1]
.TP
\fB\-\-gluecut0\fR
Glue value for lev 0 ('keep') cut [nargs=0..1] [default: 3]
.TP
\fB\-\-gluecut1\fR
Glue value for lev 1 cut ('give another shot' [nargs=0..1] [default: 6]
.TP
\fB\-\-adjustglue\fR
If more than this % of clauses is LOW glue (level 0) then lower the glue cutoff by 1 \fB\-\-\fR once and never again [nargs=0..1] [default: 0.7]
.TP
\fB\-\-everylev1\fR
Reduce lev1 clauses every N [nargs=0..1] [default: 10000]
.TP
\fB\-\-everylev2\fR
Reduce lev2 clauses every N [nargs=0..1] [default: 15000]
.TP
\fB\-\-lev1usewithin\fR
Learnt clause must be used in lev1 within this timeframe or be dropped to lev2 [nargs=0..1] [default: 70000]
.TP
\fB\-\-branchstr\fR
Branch strategy string that switches between different branch strategies while solving e.g. 'vsids1+vsids2' [nargs=0..1] [default: "vmtf+vsids"]
.TP
\fB\-\-nobansol\fR
Don't ban the solution once it's found
.TP
\fB\-\-debuglib\fR
Parse special comments to run solve/simplify during parsing of CNF
.TP
\fB\-\-breakid\fR
Run BreakID to break symmetries. [nargs=0..1] [default: true]
.TP
\fB\-\-breakideveryn\fR
Run BreakID every N simplification iterations [nargs=0..1] [default: 5]
.TP
\fB\-\-breakidmaxlits\fR
Maximum number of literals in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 3500]
.TP
\fB\-\-breakidmaxcls\fR
Maximum number of clauses in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 600]
.TP
\fB\-\-breakidmaxvars\fR
Maximum number of variables in thousands. If exceeded, BreakID will not run [nargs=0..1] [default: 300]
.TP
\fB\-\-breakidtime\fR
Maximum number of steps taken during automorphism finding. [nargs=0..1] [default: 2000]
.TP
\fB\-\-breakidcls\fR
Maximum number of breaking clauses per permutation. [nargs=0..1] [default: 50]
.TP
\fB\-\-breakidmatrix\fR
Detect matrix row interchangability [nargs=0..1] [default: true]
.TP
\fB\-\-sls\fR
Run SLS during simplification [nargs=0..1] [default: 1]
.TP
\fB\-\-slstype\fR
Which SLS to run. Allowed values: walksat, yalsat, ccnr, ccnr_yalsat [nargs=0..1] [default: "ccnr"]
.TP
\fB\-\-slsmaxmem\fR
Maximum number of MB to give to SLS solver. Doesn't run SLS solver if the memory usage would be more than this. [nargs=0..1] [default: 500]
.TP
\fB\-\-slseveryn\fR
Run SLS solver every N simplifications only [nargs=0..1] [default: 2]
.TP
\fB\-\-yalsatmems\fR
Run Yalsat with this many mems*million timeout. Limits time of yalsat run [nargs=0..1] [default: 10]
.TP
\fB\-\-walksatruns\fR
Max 'runs' for WalkSAT. Limits time of WalkSAT run [nargs=0..1] [default: 50]
.TP
\fB\-\-slsgetphase\fR
Get phase from SLS solver, set as new phase for CDCL [nargs=0..1] [default: 1]
.TP
\fB\-\-slsccnraspire\fR
Turn aspiration on/off for CCANR [nargs=0..1] [default: 1]
.TP
\fB\-\-slstobump\fR
How many variables to bump in CCNR [nargs=0..1] [default: 100]
.TP
\fB\-\-slstobumpmaxpervar\fR
How many times to bump an individual variable's activity in CCNR [nargs=0..1] [default: 100]
.TP
\fB\-\-slsbumptype\fR
How to calculate what variable to bump. 1 = clause\-based, 2 = var\-flip\-based, 3 = var\-score\-based [nargs=0..1] [default: 6]
.TP
\fB\-\-transred\fR
Remove useless binary clauses (transitive reduction) [nargs=0..1] [default: 1]
.TP
\fB\-\-intree\fR
Carry out intree\-based probing [nargs=0..1] [default: 1]
.TP
\fB\-\-intreemaxm\fR
Time in mega\-bogoprops to perform intree probing [nargs=0..1] [default: 400]
.TP
\fB\-\-otfhyper\fR
Perform hyper\-binary resolution during probing [nargs=0..1] [default: 1]
.TP
\fB\-\-schedsimp\fR
Perform simplification rounds. If 0, we never perform any. [nargs=0..1] [default: 1]
.TP
\fB\-\-presimp\fR
Perform simplification at the very start [nargs=0..1] [default: 0]
.TP
\fB\-\-allpresimp\fR
Perform simplification at EVERY start \fB\-\-\fR only matters in library mode [nargs=0..1] [default: 0]
.TP
\fB\-n\fR, \fB\-\-nonstop\fR
Never stop the search() process in class SATSolver [nargs=0..1] [default: 0]
.TP
\fB\-\-maxnumsimppersolve\fR
Maximum number of simplifiactions to perform for every solve() call. After this, no more inprocessing will take place. [nargs=0..1] [default: 25]
.TP
\fB\-\-schedule\fR
Schedule for simplification during run
.TP
\fB\-\-preschedule\fR
Schedule for simplification at startup
.TP
\fB\-\-occsimp\fR
Perform occurrence\-list\-based optimisations (variable elimination, subsumption, bounded variable addition...) [nargs=0..1] [default: 1]
.TP
\fB\-\-confbtwsimp\fR
Start first simplification after this many conflicts [nargs=0..1] [default: 40000]
.TP
\fB\-\-confbtwsimpinc\fR
Simp rounds increment by this power of N [nargs=0..1] [default: 1.4]
.TP
\fB\-\-tern\fR
Perform Ternary resolution [nargs=0..1] [default: true]
.TP
\fB\-\-terntimelim\fR
Time\-out in bogoprops M of ternary resolution as per paper 'Look\-Ahead Versus Look\-Back for Satisfiability Problems' [nargs=0..1] [default: 100]
.TP
\fB\-\-ternkeep\fR
Keep ternary resolution clauses only if they are touched within this multiple of 'lev1usewithin' [nargs=0..1] [default: 5]
.TP
\fB\-\-terncreate\fR
Create only this multiple (of linked in cls) ternary resolution clauses per simp run [nargs=0..1] [default: 0.3]
.TP
\fB\-\-ternbincreate\fR
Allow ternary resolving to generate binary clauses [nargs=0..1] [default: 0]
.TP
\fB\-\-occredmax\fR
Don't add to occur list any redundant clause larger than this [nargs=0..1] [default: 50]
.TP
\fB\-\-occredmaxmb\fR
Don't allow redundant occur size to be beyond this many MB [nargs=0..1] [default: 600]
.TP
\fB\-\-occirredmaxmb\fR
Don't allow irredundant occur size to be beyond this many MB [nargs=0..1] [default: 2500]
.TP
\fB\-\-strengthen\fR
Perform clause contraction through self\-subsuming resolution as part of the occurrence\-subsumption system [nargs=0..1] [default: 1]
.TP
\fB\-\-weakentimelim\fR
Time\-out in bogoprops M of weakeaning used [nargs=0..1] [default: 300]
.TP
\fB\-\-substimelim\fR
Time\-out in bogoprops M of subsumption of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]
.TP
\fB\-\-substimelimbinratio\fR
Ratio of subsumption time limit to spend on sub&str long clauses with bin [nargs=0..1] [default: 0.1]
.TP
\fB\-\-substimelimlongratio\fR
Ratio of subsumption time limit to spend on sub long clauses with long [nargs=0..1] [default: 0.9]
.TP
\fB\-\-strstimelim\fR
Time\-out in bogoprops M of strengthening of long clauses with long clauses, after computing occur [nargs=0..1] [default: 300]
.TP
\fB\-\-sublonggothrough\fR
How many times go through subsume [nargs=0..1] [default: 1]
.TP
\fB\-\-bva\fR
Perform bounded variable addition [nargs=0..1] [default: 1]
.TP
\fB\-\-bvaeveryn\fR
Perform BVA only every N occ\-simplify calls [nargs=0..1] [default: 7]
.TP
\fB\-\-bvalim\fR
Maximum number of variables to add by BVA per call [nargs=0..1] [default: 250000]
.TP
\fB\-\-bva2lit\fR
BVA with 2\-lit difference hack, too. Beware, this reduces the effectiveness of 1\-lit diff [nargs=0..1] [default: 1]
.TP
\fB\-\-bvato\fR
BVA time limit in bogoprops M [nargs=0..1] [default: 50]
.TP
\fB\-\-varelim\fR
Perform variable elimination as per Een and Biere [nargs=0..1] [default: 1]
.TP
\fB\-\-varelimto\fR
Var elimination bogoprops M time limit [nargs=0..1] [default: 750]
.TP
\fB\-\-varelimover\fR
Do BVE until the resulting no. of clause increase is less than X. Only power of 2 makes sense, i.e. 2,4,8... [nargs=0..1] [default: 16]
.TP
\fB\-\-emptyelim\fR
Perform empty resolvent elimination using bit\-map trick [nargs=0..1] [default: 1]
.TP
\fB\-\-varelimmaxmb\fR
Maximum extra MB of memory to use for new clauses during varelim [nargs=0..1] [default: 1000]
.TP
\fB\-\-eratio\fR
Eliminate this ratio of free variables at most per variable elimination iteration [nargs=0..1] [default: 1.6]
.TP
\fB\-\-varelimcheckres\fR
BVE should check whether resolvents subsume others and check for exact size increase [nargs=0..1] [default: 0]
.TP
\fB\-\-xor\fR
Discover long XORs [nargs=0..1] [default: 1]
.TP
\fB\-\-maxxorsize\fR
Maximum XOR size to find [nargs=0..1] [default: 7]
.TP
\fB\-\-xorfindtout\fR
Time limit for finding XORs [nargs=0..1] [default: 400]
.TP
\fB\-\-varsperxorcut\fR
Number of _real_ variables per XOR when cutting them. So 2 will have XORs of size 4 because 1 = connecting to previous, 1 = connecting to next, 2 in the midde. If the XOR is 4 long, it will be just one 4\-long XOR, no connectors [nargs=0..1] [default: 2]
.TP
\fB\-\-maxxormat\fR
Maximum matrix size (=num elements) that we should try to echelonize [nargs=0..1] [default: 400]
.TP
\fB\-\-forcepreservexors\fR
Force preserving XORs when they have been found. Easier to make sure XORs are not lost through simplifiactions such as strenghtening [nargs=0..1] [default: 1]
.TP
\fB\-\-gates\fR
Find gates. [nargs=0..1] [default: 0]
.TP
\fB\-\-printgatedot\fR
Print gate structure regularly to file 'gatesX.dot' [nargs=0..1] [default: 0]
.TP
\fB\-\-gatefindto\fR
Max time in bogoprops M to find gates [nargs=0..1] [default: 200]
.TP
\fB\-\-recur\fR
Perform recursive minimisation [nargs=0..1] [default: 1]
.TP
\fB\-\-moreminim\fR
Perform strong minimisation at conflict gen. [nargs=0..1] [default: 1]
.TP
\fB\-\-moremoreminim\fR
Perform even stronger minimisation at conflict gen. [nargs=0..1] [default: 2]
.TP
\fB\-\-moremorealways\fR
Always strong\-minimise clause [nargs=0..1] [default: 0]
.TP
\fB\-\-decbased\fR
Create decision\-based conflict clauses when the UIP clause is too large [nargs=0..1] [default: 1]
.TP
\fB\-\-updateglueonanalysis\fR
Update glues while analyzing [nargs=0..1] [default: 1]
.TP
\fB\-\-maxgluehistltlimited\fR
Maximum glue used by glue\-based restart strategy when populating glue history. [nargs=0..1] [default: 50]
.TP
\fB\-\-diffdeclevelchrono\fR
Difference in decision level is more than this, perform chonological backtracking instead of non\-chronological backtracking. Giving \fB\-1\fR means it is never turned on (overrides '\-\-confltochrono \fB\-1\fR' in this case). [nargs=0..1] [default: 20]
.TP
\fB\-\-verbstat\fR
Change verbosity of statistics at the end of the solving [0..3] [nargs=0..1] [default: 2]
.TP
\fB\-\-verbrestart\fR
Print more thorough, but different stats [nargs=0..1] [default: 0]
.TP
\fB\-\-verballrestarts\fR
Print a line for every restart [nargs=0..1] [default: 0]
.TP
\fB\-\-printsol\fR,s
Print assignment if solution is SAT [nargs=0..1] [default: 1]
.TP
\fB\-\-restartprint\fR
Print restart status lines at least every N conflicts [nargs=0..1] [default: 8192]
.TP
\fB\-\-distill\fR
Regularly execute clause distillation [nargs=0..1] [default: 1]
.TP
\fB\-\-distillbin\fR
Regularly execute clause distillation [nargs=0..1] [default: 1]
.TP
\fB\-\-distillmaxm\fR
Maximum number of Mega\-bogoprops(~time) to spend on vivifying/distilling long cls by enqueueing and propagating [nargs=0..1] [default: 20]
.TP
\fB\-\-distillincconf\fR
Multiplier for current number of conflicts OTF distill [nargs=0..1] [default: 0.1]
.TP
\fB\-\-distillminconf\fR
Minimum number of conflicts between OTF distill [nargs=0..1] [default: 10000]
.TP
\fB\-\-distilltier0ratio\fR
How much of tier 0 to distill [nargs=0..1] [default: 10]
.TP
\fB\-\-distilltier1ratio\fR
How much of tier 1 to distill [nargs=0..1] [default: 0.03]
.TP
\fB\-\-distillirredalsoremratio\fR
How much of irred to distill when doing also removal [nargs=0..1] [default: 1.2]
.TP
\fB\-\-distillirrednoremratio\fR
How much of irred to distill when doing no removal [nargs=0..1] [default: 1]
.TP
\fB\-\-distillshuffleeveryn\fR
Shuffle to\-be\-distilled clauses every N cases randomly [nargs=0..1] [default: 3]
.TP
\fB\-\-distillsort\fR
Distill sorting type [nargs=0..1] [default: 1]
.TP
\fB\-\-renumber\fR
Renumber variables to increase CPU cache efficiency [nargs=0..1] [default: 1]
.TP
\fB\-\-mustconsolidate\fR
Always consolidate, even if not useful. This is used for debugging ONLY [nargs=0..1] [default: 0]
.TP
\fB\-\-savemem\fR
Save memory by deallocating variable space after renumbering. Only works if renumbering is active. [nargs=0..1] [default: 1]
.TP
\fB\-\-mustrenumber\fR
Treat all 'renumber' strategies as 'must\-renumber' [nargs=0..1] [default: 0]
.TP
\fB\-\-fullwatchconseveryn\fR
Consolidate watchlists fully once every N conflicts. Scheduled during simplification rounds. [nargs=0..1] [default: 4000000]
.TP
\fB\-\-strmaxt\fR
Maximum MBP to spend on distilling long irred cls through watches [nargs=0..1] [default: 20]
.TP
\fB\-\-implicitmanip\fR
Subsume and strengthen implicit clauses with each other [nargs=0..1] [default: 1]
.TP
\fB\-\-implsubsto\fR
Timeout (in bogoprop Millions) of implicit subsumption [nargs=0..1] [default: 100]
.TP
\fB\-\-implstrto\fR
Timeout (in bogoprop Millions) of implicit strengthening [nargs=0..1] [default: 200]
.TP
\fB\-\-cardfind\fR
Find cardinality constraints [nargs=0..1] [default: 0]
.TP
\fB\-\-sync\fR
Sync threads every N conflicts [nargs=0..1] [default: 7000]
.TP
\fB\-\-clearinter\fR
Interrupt threads cleanly, all the time [nargs=0..1] [default: 0]
.TP
\fB\-\-zero\-exit\-status\fR
Exit with status zero in case the solving has finished without an issue
.TP
\fB\-\-printtimes\fR
Print time it took for each simplification run. If set to 0, logs are easier to compare [nargs=0..1] [default: 1]
.TP
\fB\-\-maxsccdepth\fR
The maximum for scc search depth [nargs=0..1] [default: 10000]
.TP
\fB\-\-simfrat\fR
Simulate FRAT [nargs=0..1] [default: 0]
.TP
\fB\-\-sampling\fR
Sampling vars, separated by comma [nargs=0..1] [default: ""]
.TP
\fB\-\-onlysampling\fR
Print and ban(!) solutions' vars only in 'c ind' or as \fB\-\-sampling\fR '...'
.TP
\fB\-\-assump\fR
Assumptions file [nargs=0..1] [default: ""]
.TP
\fB\-\-maxmatrixrows\fR
Set maximum no. of rows for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 2000]
.TP
\fB\-\-maxmatrixcols\fR
Set maximum no. of columns for gaussian matrix. Too large matricesshould bee discarded for reasons of efficiency [nargs=0..1] [default: 1000]
.TP
\fB\-\-autodisablegauss\fR
Automatically disable gauss when performing badly [nargs=0..1] [default: true]
.TP
\fB\-\-minmatrixrows\fR
Set minimum no. of rows for gaussian matrix. Normally, too small matrices are discarded for reasons of efficiency [nargs=0..1] [default: 3]
.TP
\fB\-\-maxnummatrices\fR
Maximum number of matrices to treat. [nargs=0..1] [default: 5]
.TP
\fB\-\-detachxor\fR
Detach and reattach XORs [nargs=0..1] [default: false]
.TP
\fB\-\-useallmatrixes\fR
Force using all matrices [nargs=0..1] [default: false]
.TP
\fB\-\-detachverb\fR
If set, verbosity for XOR detach code is upped, ignoring normal verbosity [nargs=0..1] [default: 0]
.TP
\fB\-\-gaussusefulcutoff\fR
Turn off Gauss if less than this many usefulenss ratio is recorded [nargs=0..1] [default: 0.2]
.TP
\fB\-\-dumpresult\fR
Write solution(s) to this file
.SS "Normal run schedules:"
.IP
Default schedule: scc\-vrepl,sub\-impl,breakid,occ\-backw\-sub\-str,occ\-clean\-implicit,occ\-bve,occ\-bva,occ\-ternary\-res,occ\-xor,card\-find,cl\-consolidate,scc\-vrepl,renumber,bosphorus,louvain\-comms
.IP
Schedule at startup: sub\-impl, occ\-backw\-sub,scc\-vrepl,breakid, occ\-bve,occ\-xor
.SH "SEE ALSO"
The full documentation for
.B cryptominisat5
is maintained as a Texinfo manual.  If the
.B info
and
.B cryptominisat5
programs are properly installed at your site, the command
.IP
.B info cryptominisat5
.PP
should give you access to the complete manual.